KI entschlüsselt Gödels Notizbücher: Hunderte unbekannte Sätze entdeckt

Worum es geht

Kurt Gödel (1906–1978) gilt als einer der originellsten Denker des 20. Jahrhunderts. Seine beiden Unvollständigkeitssätze von 1931 haben die Mathematik verändert und den Weg für die Computertheorie geebnet. Nach den bahnbrechenden Arbeiten der 1930er-Jahre veröffentlichte Gödel nur noch wenige Aufsätze. Sein unveröffentlichter Nachlass umfasst aber Zehntausende Seiten.

Wie der Guardian berichtet, hat der finnische Logiker Jan von Plato von der Universität Helsinki einen Teil dieses Nachlasses jetzt mit Hilfe des KI-Modells Claude von Anthropic ausgewertet. Es geht um 16 Notizbücher, die Gödel Anfang der 1940er-Jahre schrieb und die als „Workbooks“ bekannt sind: 1.009 eng beschriebene Seiten über Mathematik und Logik. Nach von Platos Angaben enthalten sie Hunderte bewiesene oder skizzierte Sätze, von denen bisher niemand wusste.

„Ich war fassungslos. Die Workbooks enthalten nicht nur Dutzende Vorwegnahmen von Ergebnissen, die erst in den 70er- und 80er-Jahren bekannt wurden, sondern auch 14 Themen der Logik, die nie weiterverfolgt wurden. Gödel war seiner Zeit weit voraus.“

Eine Seite pro Woche: das Problem mit der Kurzschrift

Die Notizbücher sind schwer zu lesen. Gödel schrieb großteils in Gabelsberger, einer deutschen Kurzschrift, die schon zu seiner Zeit veraltet war. Von Plato begann das Projekt 2017, kurz vor seiner Pflichtpensionierung. Mit einem Augenzwinkern erklärt er, er habe sich damit unverzichtbar machen wollen. Der Europäische Forschungsrat förderte das Projekt mit 2,5 Millionen Euro. Von Plato brachte sich die Kurzschrift selbst bei. Er sei „einer von nur sechs Menschen weltweit, die sie lesen können“, sagt er. Dazu stellte er ein kleines Team zusammen.

Das Lesen war das eine, das mathematische Verständnis das andere. Hier ging es nur sehr langsam voran, etwa eine Seite pro Woche. Den Anstoß zur KI gaben Informatiker, die von Plato im August auf einer Konferenz in Frankreich über KI und automatisches Beweisen traf. Zurück in Helsinki gab er Claude seine eigenen Abschriften der Workbooks. Dazu kamen sechs Bücher, die er selbst über Gödel geschrieben hatte, und weitere Fachliteratur. Die KI hat also nicht die Kurzschrift-Originale entziffert, sondern mit den Transkriptionen gearbeitet, die Menschen angefertigt hatten.

650 Seiten in wenigen Tagen

Nach wenigen Tagen hatte von Plato eine 650 Seiten lange Erläuterung der gesamten Notizbücher vor sich. Er betont, dass er sie Seite für Seite prüfen musste. Trotzdem sei das eine Arbeit, die für Menschen praktisch unmöglich sei:

„Menschen lesen eine Seite nach der anderen und vergessen dabei Dinge. Wir brauchen ein Jahr für etwa 50 Seiten. Die KI kann alle Teile auf tausend Seiten miteinander verbinden. Sie sieht Gödels Schriften als ein Ganzes.“

Diese Stärke kommt bei solchen Aufgaben besonders zum Tragen. Große Sprachmodelle können sehr lange Texte auf einmal im Blick behalten und Bezüge zwischen weit auseinanderliegenden Stellen herstellen. Ein menschlicher Leser müsste sich dafür mühsam Notizen machen.

Der fast fertige Beweis zum Auswahlaxiom

Die erste Frage an Claude hatte einen historischen Hintergrund. Gödels Unvollständigkeitssätze zeigen, dass es in jedem ausreichend mächtigen mathematischen System wahre Aussagen gibt, die sich innerhalb dieses Systems weder beweisen noch widerlegen lassen. Solche Aussagen heißen „unabhängig“. 1966 erhielt der US-Mathematiker Paul Cohen die Fields-Medaille, die höchste Auszeichnung der Mathematik. Er hatte gezeigt, dass zwei berühmte Aussagen der Mengenlehre unabhängig sind: die Kontinuumshypothese und das Auswahlaxiom. Das Auswahlaxiom ist ein Grundsatz, nach dem man aus beliebig vielen nichtleeren Mengen immer je ein Element auswählen kann.

Gödel erklärte damals, er habe das schon in den 1940er-Jahren bewiesen. Als Kollegen ihn um den Beweis baten, konnte er ihn aus seinen Notizen aber nicht rekonstruieren. Von Plato wollte deshalb wissen, ob die Workbooks einen solchen Beweis enthalten. Die Antwort lautete: fast.

„Er war nur einen Schritt entfernt. Es gibt eine Definition, die Gödel falsch hatte, aber zwei Jahre vorher hatte er die richtige. Er wäre also wohl darauf gekommen, wenn er noch ein paar Monate weitergemacht hätte.“

Den rekonstruierten Beweis ließ von Plato durch Coq laufen. Das ist ein Beweisassistent, also ein Programm, das jeden logischen Schritt eines Beweises maschinell prüft. Der Beweis bestand die Prüfung. Von Plato glaubt, dass Gödel mit einer Veröffentlichung die Fields-Medaille von 1950 hätte bekommen können. Im Guardian steht zwar „1940“, damals wurde die Medaille aber kriegsbedingt nicht vergeben. Welche Verleihung gemeint ist, bleibt deshalb unklar. Vielleicht habe Gödel bei Cohens Auszeichnung das Gefühl gehabt, etwas verpasst zu haben, sagt von Plato. Er lobt vor allem Gödels Arbeitsweise. Gödel spiele nicht mit Formeln und hoffe auf ein Ergebnis, sondern gehe von klaren Ideen aus und arbeite sie methodisch ab.

663 Sätze, maschinell geprüft

Anschließend ließ von Plato Claude alle Sätze heraussuchen, für die Gödel einen Beweis, eine Beweisskizze oder wenigstens eine Beweisidee notiert hatte. Die KI fand 663. Auch diese wurden in Coq überprüft:

Dass etwa 50 Sätze falsch sind, überrascht von Plato nicht. Gödel selbst schrieb beim Wiederlesen gelegentlich „falsch!“ oder „schlecht!“ an den Rand. Nach Claudes Analyse enthalten die Workbooks außerdem mehr als ein Dutzend Themen aus Logik und Grundlagen der Mathematik, die in den über 80 Jahren seit ihrer Niederschrift niemand aufgegriffen hat. Als Nächstes will sich von Plato Gödels Notizbücher zu Physik und Kosmologie vornehmen, die er als „unbekanntes Terrain“ bezeichnet.

Gödel: Genie mit tragischem Ende

Gödel floh 1940 vor den Nationalsozialisten aus Österreich und ließ sich in Princeton nieder. Am Institute for Advanced Study war er eng mit Albert Einstein befreundet. Seine Unvollständigkeitssätze waren ein Schlag für die Logiker vor ihm, die gehofft hatten, alle mathematischen Wahrheiten seien beweisbar. Sie gaben dem Fach aber auch eine neue Richtung und inspirierten Alan Turing zu seinem Aufsatz von 1936, mit dem die moderne Berechenbarkeitstheorie begann. In seinen späteren Jahren litt Gödel zunehmend unter Verfolgungsangst. Er aß nur noch, was seine Frau gekocht hatte, und starb 1978 an Unterernährung.

Einordnung

Die Geschichte zeigt einen nüchternen, aber starken Nutzen von Sprachmodellen in der Forschung. Sie lösen keine offenen Probleme aus dem Nichts. Sie erschließen riesige, schwer zugängliche Textmengen und verknüpfen sie. Wichtig ist der Ablauf: Ein Experte liefert die Transkription und das Hintergrundwissen, die KI fasst zusammen und rekonstruiert, und am Ende prüft ein formales Werkzeug wie Coq das Ergebnis. Diese Kombination verringert das bekannte Risiko, dass Sprachmodelle plausibel klingende Fehler produzieren.

Einiges bleibt allerdings offen. Die Ergebnisse stammen bisher nur aus von Platos Darstellung im Guardian. Eine begutachtete Veröffentlichung wird nicht erwähnt. Joel David Hamkins, Logikprofessor an der University of Notre Dame, hat die Rekonstruktion noch nicht gesehen. Falls sie sich bestätige, sei sie „bemerkenswert und historisch interessant“. Er stellt aber die entscheidende Frage: Wie viel stammt von Claude und wie viel von Gödel? Das sei „eine Aufgabe für die Historiker“. Wenn Claude eine Lücke in Gödels Beweis selbst gefüllt hat, ist der Beweis eben nicht ganz Gödels.

Auch die Würdigung schränkt Hamkins ein:

„Dass es dort Dinge gibt, die Cohens Beweis ähneln, heißt nicht, dass Gödel ihn hatte. Es zeigt, dass er auf dem Weg war. Für Arbeit, von der man niemandem erzählt, bekommt man keine Anerkennung.“

Dazu kommt eine methodische Frage. Ein Coq-Beweis zeigt, dass die formalisierte Aussage stimmt. Ob die Formalisierung genau das trifft, was Gödel gemeint hat, muss ein Mensch beurteilen. Gerade bei den rund 200 „reparierten“ Sätzen ist das eine Frage der Auslegung. Trotzdem: Wenn sich die Zahlen bestätigen, hat die KI in Tagen erledigt, wofür ein menschliches Team bei einer Seite pro Woche rund zwanzig Jahre gebraucht hätte. Das macht Nachlässe zugänglich, die bisher kaum jemand lesen konnte.