OpenAI hat am 26. Oktober gleich drei Forschungsergebnisse vorgestellt, die von seinen KI-Modellen stammen sollen. Sie gehören zur theoretischen Informatik, zur harmonischen Analysis und zur mathematischen Physik. Das gewichtigste ist ein Beweis, dass die Exponentialzeit-Hypothese (ETH) nicht gilt. Welches Modell zum Einsatz kam, nennt das Unternehmen nicht; es spricht lediglich von „KI-Modellen von OpenAI“ und betont, alle drei Ergebnisse müssten von der Fachwelt noch unabhängig bestätigt werden.
ETH: das Fundament für Hunderte Arbeiten
Die Exponentialzeit-Hypothese betrifft die Rechenschwere des Erfüllbarkeitsproblems für boolesche Formeln (3-SAT): Grob gesagt behauptet sie, dass sich diese Probleme nicht in subexponentieller Zeit lösen lassen. Sie ist stärker als „P ungleich NP“ und zugleich handlicher. Seit Jahrzehnten gilt sie als Standardannahme, und die Schranken in Hunderten Arbeiten zu Graphentheorie, Computational Biology, Datenbanken und algorithmischer Geometrie beruhen auf ihr.
Nach der von OpenAI veröffentlichten Zeitleiste erzeugte das Modell den Beweis in natürlicher Sprache am 16. Oktober und schloss die Lean-Formalisierung am Tag darauf ab. Beteiligt waren Russell Impagliazzo und Ramamohan Paturi von der University of California, San Diego sowie Ryan Williams vom Massachusetts Institute of Technology. Die beiden Erstgenannten gehören zu den Urhebern der ETH.
Wie bekannt wurde, stellten die Forscher OpenAI zwei Bedingungen: die vollständige Offenlegung aller Rohdaten und die Finanzierung einer wissenschaftlichen Konferenz, die sich speziell mit den Folgen dieses Ergebnisses für die Informatik befasst. OpenAI sagte beides zu. Hält der Beweis der Prüfung stand, müssten all jene Arbeiten, die ETH voraussetzen, einzeln neu bewertet werden: Welche Schlussfolgerungen verlieren nur ihre Voraussetzung, welche lassen sich mit anderen Annahmen retten? Das wäre ein erheblicher Aufwand.
Kakeya-Vermutung: eine Linie, die chinesischen Lesern vertraut ist
Das zweite Ergebnis ist der Beweis der Local-Smoothing-Vermutung in allen Dimensionen, aus dem sich die Kakeya-Vermutung und die Stein-Restriktionsvermutung in allen Dimensionen ableiten. Entscheidend ist dabei eine vom Modell konstruierte partielle Hilfsdifferentialgleichung. Laut OpenAI lag der Beweis am 18. Oktober vor, die Lean-Formalisierung folgte am nächsten Tag; sowohl die Fassung in natürlicher Sprache als auch die Lean-Dateien sind auf GitHub abrufbar.
Diese Forschungslinie ist chinesischen Lesern nicht fremd. Die Local-Smoothing-Vermutung formulierte Christopher Sogge 1991; 2019 bewiesen Larry Guth, Hong Wang und Ruixiang Zhang den zweidimensionalen Fall; 2025 bewiesen Hong Wang und Joshua Zahl die dreidimensionale Kakeya-Vermutung, was damals als einer der wichtigsten Fortschritte der harmonischen Analysis seit Jahren galt. Der Sprung von drei Dimensionen auf alle Dimensionen ist gewaltig; wie externe Mathematiker ihn einschätzen, ist öffentlich bislang nicht zu erfahren.
Yang-Mills: nur von Experten gegengelesen
Das dritte Ergebnis gehört zur mathematischen Physik. Die Arbeit zeigt im streng mathematischen Sinn, dass im vierdimensionalen Raum bestimmte wechselwirkende Quantenfeldtheorien existieren, die sowohl Eichfelder als auch Fermionen enthalten und die Quantenchromodynamik einschließen. Nebenbei behandelt sie ein Teilproblem der Existenz der reinen Yang-Mills-Theorie. Existenz und Massenlücke der reinen Yang-Mills-Theorie gehören zu den Millennium-Problemen des Clay Mathematics Institute.
Die Methode folgt dem Ansatz der konstruktiven Quantenfeldtheorie von Tadeusz Balaban. Da sich das Standardmodell nicht ohne Weiteres auf beliebig kurze Abstandsskalen übertragen lässt, bezieht sich der Beweis auf die einfachste Große Vereinheitlichte Theorie, die die Eichfelder und Fermionen des Standardmodells enthält. Das Gegenlesen leitete der Nobelpreisträger David Gross, beteiligt waren Michael Douglas, Arthur Jaffe, Igor Klebanov und Nikita Nekrasov. Dieses Ergebnis wurde nicht formal verifiziert.
Von Mai bis Oktober
Reiht man OpenAIs mathematische Veröffentlichungen dieses Jahres aneinander, wird das Tempo schneller, und die Gegenstände ändern sich. Im Mai ging es um ein achtzig Jahre altes Erdős-Problem; im September um die Glattheit der Navier-Stokes-Gleichungen, ebenfalls mit Lean-Dateien, aber damals ohne unabhängige Verifikation durch Mathematiker; diesmal geht es um eine Annahme der Komplexitätstheorie, auf der unzählige Folgearbeiten fußen, und zum ersten Mal stehen die Urheber der Annahme selbst auf der Liste der Mitwirkenden.
Auch die Verifikation unterscheidet sich: Für die zwei mathematischen Ergebnisse liegen maschinenprüfbare Lean-Beweise vor, die physikalische Arbeit kann sich nur auf menschliches Gegenlesen stützen. Lean garantiert, dass die Herleitung lückenlos ist, vorausgesetzt, die Aussage selbst wurde bei der Formalisierung nicht verfälscht. Das lässt sich erst bestätigen, wenn unabhängige Teams die Dateien Zeile für Zeile gelesen haben.
Quellen: Forschungsmitteilung von OpenAI, CocoLoop, ITHome; öffentlich auf GitHub bereitgestellte Lean-Formalisierungen zur Prüfung von Beweisgegenstand und Verifikationsweg.