Der österreichische Logiker Kurt Gödel hat 1.009 Seiten dicht beschriebenen Text hinterlassen, großenteils in einer veralteten Kurzschrift. Wie The Guardian berichtet, sollen darin Hunderte bewiesene Theoreme stehen, von denen bisher niemand wusste. Möglich wurde die Entdeckung durch ein Projekt der Universität Helsinki, das der finnische Logiker Jan von Plato leitet.
Gödels Unvollständigkeitssätze, 1931 veröffentlicht, veränderten die Mathematik grundlegend und ebneten den Weg für das digitale Zeitalter. Nach seinen bahnbrechenden Ergebnissen der 1930er-Jahre veröffentlichte Gödel nur noch wenige Arbeiten. Sein unveröffentlichtes Werk umfasst nach Angaben der Quelle zehntausende Seiten und ist für Wissenschaftshistoriker von großem Interesse.
Von Plato arbeitet seit 2017 an den sechzehn Notizbüchern, die Gödel Anfang der 1940er-Jahre schrieb. Die sogenannten Workbooks befassen sich mit Mathematik und Logik und sind größtenteils in der Gabelsberger-Kurzschrift verfasst, die schon zu Gödels Zeiten veraltet war. Der Fortschritt war lange mühsam, etwa eine Seite pro Woche. Erst im September zog von Plato das KI-Modell Claude hinzu. Binnen weniger Tage lieferte es eine umfassende Zusammenfassung des gesamten Materials.
Von Plato sagte, er sei überwältigt gewesen. Die Notizbücher enthielten dutzende Vorwegnahmen von Ergebnissen, die erst in den 1970er- und 1980er-Jahren bekannt wurden. Außerdem fänden sich darin vierzehn Themen der Logik, die nie weiterverfolgt wurden. Gödel sei seiner Zeit weit voraus gewesen.
Von Plato begann sein Gödel-Projekt nach eigenen Angaben 2017, weil ihm der verpflichtende Ruhestand an der Universität Helsinki bevorstand. Er erhielt einen Förderbetrag von 2,5 Millionen Euro des Europäischen Forschungsrats, brachte sich selbst die Gabelsberger-Kurzschrift bei und stellte ein kleines Team zusammen. Nach eigenen Worten gehört er weltweit zu nur sechs Menschen, die sie lesen können.
Im August hatte von Plato auf einer Konferenz in Frankreich über KI und automatisches Beweisen Informatiker getroffen, die ihm vorschlugen, Claude einzusetzen. Er gab dem Modell seine Transkriptionen der Workbooks sowie sechs eigene Bücher über Gödel und weitere wissenschaftliche Fachliteratur. Claude erstellte daraufhin eine 650 Seiten lange Erläuterung der Notizbücher, die Seite für Seite kontrolliert werden musste. Von Plato erklärte, ein Mensch brauche für etwa 50 Seiten ein ganzes Jahr und könne nicht alle Zusammenhänge im Kopf behalten. Die KI könne dagegen tausend Seiten miteinander verbinden und Gödels Schriften als ein Ganzes betrachten.
Die erste Aufgabe für Claude war, ob die Notizbücher einen Beweis der Unabhängigkeit des Auswahlaxioms enthalten. Der Mathematiker Paul Cohen hatte dafür 1966 die Fields-Medaille erhalten, die höchste Auszeichnung der Mathematik, unter anderem für den Nachweis der Unabhängigkeit der Kontinuumshypothese und des Auswahlaxioms. Gödel hatte damals erklärt, er habe das Ergebnis bereits in den 1940er-Jahren bewiesen. Auf Nachfrage von Kollegen konnte er den Beweis jedoch nicht aus seinen Notizen rekonstruieren. Claude antwortete laut von Plato, Gödel sei dem Beweis „fast“ nahe gewesen: Nur ein Schritt habe gefehlt, eine Definition sei falsch gewesen. Von Plato glaubt, Gödel hätte mit einigen Monaten weiterer Arbeit die richtige Definition gefunden. Die Architektur des Beweises nannte er außergewöhnlich.
Die rekonstruierte Beweisführung prüfte von Plato mit dem Beweisassistenten Coq, der sie nach seinen Angaben bestand. Anschließend ließ er Claude alle Theoreme herausfiltern, zu denen Gödel einen Beweis, einen Beweisentwurf oder eine Beweisidee notiert hatte. Claude fand 663 solcher Ergebnisse. Laut von Plato wurden etwa 400 davon in der angegebenen Form bestätigt, etwa 200 mussten korrigiert werden, und etwa 50 waren falsch. Das überrasche ihn nicht, sagte er, denn Gödel habe beim Durchlesen seiner Notizen gelegentlich am Rand „falsch!“ oder „schlecht!“ vermerkt.
Joel David Hamkins, Logikprofessor an der University of Notre Dame in Indiana, hat die Rekonstruktion nach eigenen Angaben nicht gesehen. Sollte sie standhalten, sei sie bemerkenswert und historisch interessant, sagte er. Wie viel vom Ergebnis auf Claude und wie viel auf Gödel zurückgehe, sei eine Frage für Historiker. Hamkins betonte, dass Ähnlichkeiten mit Cohens Beweis nicht bedeuteten, dass Gödel ihn besessen habe. Die Notizbücher zeigten, dass Gödel auf dem Weg dorthin gewesen sei. Anerkennung erhalte nur, wer seine Arbeit anderen mitteile.
Von Plato erwartet weitere Funde. Die Notizbücher enthielten nach Angaben von Claude mehr als ein Dutzend Themen aus der Logik und den Grundlagen der Mathematik, die in den über 80 Jahren seit ihrer Niederschrift nicht entdeckt wurden. Nach Abschluss seiner laufenden Logikprojekte will von Plato Gödels physikalische und kosmologische Notizbücher untersuchen.
Kommentare (0)