Claude hilft einem Logiker aus Helsinki, Gödels in Kurzschrift verfasste Arbeitshefte zu lesen – und stößt auf Hunderte Theoreme

The Guardian berichtet, dass Jan von Plato, der seit 2017 ein Projekt der Universität Helsinki zu Kurt Gödels 16 „Arbeitsheften“ aus den frühen 1940er-Jahren leitet (1.009 Seiten, größtenteils in der veralteten Gabelsberger-Kurzschrift), Claude im September seine Transkriptionen, seine früheren Bücher über Gödel und die Sekundärliteratur übergab. Laut von Plato erstellte Claude innerhalb weniger Tage eine 650-seitige Erläuterung der Arbeitshefte, die seiner Aussage nach Seite für Seite überprüft werden musste.

Was von Plato zufolge dabei herauskam. Auf die Frage, ob die Arbeitshefte einen Beweis dafür enthalten, dass das Auswahlaxiom unabhängig ist, rekonstruierte Claude einen Beweis, der laut von Plato „fast“ vollständig ist – mit einer falschen Definition, die Gödel zwei Jahre zuvor noch richtig angegeben hatte. Von Plato sagt, der rekonstruierte Beweis habe den Coq-Beweisassistenten bestanden. Auf die Frage, alle Theoreme aufzulisten, die Gödel bewiesen, skizziert oder als Idee festgehalten hatte, nannte Claude 663. Von Plato zufolge wurden etwa 400 in der angegebenen Form in Coq verifiziert, etwa 200 mussten korrigiert werden, und etwa 50 waren falsch. Außerdem habe Claude mehr als ein Dutzend logische Themen identifiziert, die bisher nicht weiterverfolgt worden seien.

Einschränkungen. Joel David Hamkins von der University of Notre Dame, der die Rekonstruktion nicht gesehen hatte, sagte gegenüber The Guardian, falls sie Bestand habe, sei sie „bemerkenswert und historisch interessant“. Wie viel davon Claude und wie viel Gödel zuzuschreiben sei, sei jedoch eine Frage für Historiker; und eine Ähnlichkeit mit Cohens Beweis bedeute nicht, dass Gödel ihn bereits hatte.