Deshalb hat OpenAI externe Fachleute gebeten, die Ergebnisse als "Hirten" zu begleiten. Auf deren Rat geht das Unternehmen in jedem Fach anders vor. Die Beweise aus Mathematik und Informatik hat OpenAI nach eigenen Angaben zudem in Lean übertragen.
Lean ist eine Programmiersprache, in der ein Computer jeden Schritt eines Beweises nachprüft. Fehlerfrei ist das Ergebnis damit aber nicht zwingend. Lean prüft nur, ob der Beweis die Aussage belegt, die in Lean formuliert wurde. Ob diese Aussage wirklich das gemeinte Problem beschreibt, müssen Fachleute klären.
Eine verbreitete Annahme der Informatik soll falsch sein
Im Kern des Informatik-Ergebnisses steht eine Annahme, die Exponentialzeit-Hypothese (ETH). Sie betrifft das sogenannte Erfüllbarkeitsproblem der Aussagenlogik, kurz SAT. Dabei geht es um eine logische Formel, deren Variablen nur wahr oder falsch sein können. Gefragt ist, ob man die Variablen so wählen kann, dass die ganze Formel wahr wird.
Bei wenigen Variablen kann man einfach alle Möglichkeiten ausprobieren. Doch jede weitere Variable verdoppelt die Zahl der Möglichkeiten. Bei 100 Variablen ergibt sich bereits eine Zahl mit 31 Stellen.
Die ETH besagt vereinfacht, dass es keinen grundlegend besseren Weg gibt. Man kann das Ausprobieren zwar beschleunigen. Die Rechenzeit wächst im schlimmsten Fall aber trotzdem exponentiell, also mit jeder weiteren Variable um einen festen Faktor.
Laut OpenAI sei das Erfüllbarkeitsproblem eng mit dem P-NP-Problem verwandt. Dahinter steht die berühmte offene Frage: Wenn sich die Lösung eines Problems schnell überprüfen lässt, lässt sich das Problem dann auch schnell lösen? Bei SAT ist das Überprüfen leicht: Man setzt einen Vorschlag einfach ein und rechnet nach. Schwer ist es, einen passenden Vorschlag zu finden.
SAT gilt als Musterbeispiel für schwere Probleme dieser Art. Ein schnelles Verfahren dafür würde auf einen Schlag Tausende weitere Probleme schnell lösbar machen. Die meisten Fachleute vermuten, dass es kein solches Verfahren gibt. Diese Vermutung heißt kurz "P ungleich NP".
Die ETH geht noch weiter als diese Vermutung: Sie sagt nicht nur, dass SAT schwer ist, sondern auch, wie schwer. Fällt sie, kann P ungleich NP trotzdem stimmen. Schwere Probleme werden dadurch also nicht automatisch leicht.
Die ETH galt weithin als wahr. Hunderte Arbeiten aus Graphentheorie, computergestützter Biologie, Datenbanken oder algorithmischer Geometrie bauen auf ihr auf. Sie zeigen etwa, dass sich ein Problem nicht schneller als in einer bestimmten Zeit lösen lässt, falls die ETH stimmt.
Nun habe das System bewiesen, dass die ETH falsch sei, schreibt OpenAI. Hält der Beweis, verlieren diese Arbeiten ihre Grundlage. Ihre Ergebnisse sind dann nicht automatisch falsch, aber auch nicht mehr belegt.
Laut OpenAI könne das Ergebnis bei der Suche nach besseren Algorithmen helfen. Bis daraus praktische Verbesserungen werden, sei aber noch erhebliche Forschung nötig.
Der praktische Nutzen ist ungewiss, die Folgen für die Theorie wären groß
In der Praxis spielt SAT eine große Rolle. Es gibt spezielle Programme dafür, sogenannte SAT-Solver. Sie prüfen etwa Chipentwürfe auf Fehler oder testen Software.
Oft schaffen sie schon heute Formeln mit Millionen Variablen. Denn Formeln aus echten Anwendungen sind meist viel leichter als der schlimmste Fall, um den es bei der ETH geht. Wird nur der schlimmste Fall schneller lösbar, hilft das solchen Programmen daher nicht automatisch.
Ähnlich vorsichtig äußert sich Ryan Williams, Professor am MIT, bei X. Ein Nutzer fragte ihn, was gewöhnliche Entwickler zuerst merken würden. Man wisse das noch nicht, antwortete Williams. Beim aktuellen Tempo sei es plausibel, dass es binnen zwölf Monaten einen ernsthaften Fortschritt beim praktischen Lösen von SAT gebe. "Oder wir sehen vielleicht nichts dergleichen. Ich weiß es wirklich nicht", räumt er ein.
Auch innerhalb der Komplexitätstheorie hätte das Ergebnis Folgen. Sie betreffen Schaltkreise, also Netze aus einfachen Logikbausteinen wie UND, ODER und NICHT. Sollte OpenAIs Ergebnis halten, folge daraus laut Williams, dass sich eine bestimmte Klasse sehr aufwendiger Probleme nicht mit kleinen Schaltkreisen lösen lasse. Klein heißt hier: Bei doppelt so langer Eingabe braucht der Schaltkreis höchstens etwa doppelt so viele Bausteine.
Die Erfinder der ETH prüfen ihre Widerlegung
Williams soll das Ergebnis gemeinsam mit Russell Impagliazzo und Ramamohan Paturi von der UC San Diego unabhängig prüfen und erklären. Impagliazzo und Paturi haben die ETH ursprünglich zusammen mit Francis Zane aufgestellt. Die Gruppe habe keine Verschwiegenheitserklärungen unterschrieben, arbeite unbezahlt und wolle Zwischenergebnisse laufend teilen, schreibt Williams.
In einem offenen Brief stellen die drei zudem klar, dass ihre Beteiligung keine Bestätigung der Behauptung sei. Ein Ergebnis dieser Tragweite brauche eine sorgfältige, unabhängige Prüfung.
Auf Bitte der Gruppe veröffentlicht OpenAI alle Rohdaten, darunter den ausformulierten Beweis und den Lean-Beweis. Außerdem hat das Unternehmen zugesagt, eine Konferenz zu den Folgen für das Fach zu finanzieren.
Eine Vermutung über Wellen soll in jeder Dimension gelten
Das Mathematik-Ergebnis betrifft eine Vermutung über Wellen, wie sie bei Schall, Licht oder Erdbeben auftreten. Der Mathematiker Christopher Sogge stellte diese Vermutung 1991 auf.
Wellen können sich an einer Stelle bündeln, ähnlich wie Licht im Brennpunkt einer Lupe. Laut der Vermutung hält eine extreme Bündelung aber nur kurz an. Über die Zeit gemittelt verhalten sich Wellen deshalb glatter, also gleichmäßiger, als der Extremfall vermuten ließe. Daher der Name: Vermutung der lokalen Glättung, kurz Glättungsvermutung.
Bewiesen war die Glättungsvermutung bisher nur in zwei Dimensionen, also für Wellen auf einer Fläche wie einer Wasseroberfläche. Das gelang 2019 Guth, Wang und Zhang. Laut OpenAI hätten die Modelle des Unternehmens nun einen Beweis für jede Dimension erzeugt, also auch für Wellen im Raum und in gedachten Räumen mit noch mehr Dimensionen.
Das Ergebnis reicht laut OpenAI über die Wellen hinaus. Weil die Glättungsvermutung so grundlegend sei, folgen aus ihr zwei weitere bekannte Vermutungen: die Kakeya-Vermutung aus der Geometrie und Steins Restriktionsvermutung aus der Fourier-Analyse. Die Fourier-Analyse zerlegt Signale wie Töne in einzelne Schwingungen. Wer die Glättungsvermutung beweist, hat damit automatisch auch diese beiden bewiesen.
Wie schwer schon diese Folgerungen sind, zeigt die Kakeya-Vermutung: Für drei Dimensionen haben Wang und Zahl sie erst 2025 bewiesen. Laut OpenAI wären nun beide Vermutungen in allen Dimensionen gelöst.
Anders als bei den beiden anderen Ergebnissen begleitet hier keine feste Gruppe den Beweis. OpenAI hat sich nach eigenen Angaben zwar an eine externe Fachperson gewandt, um eine solche Zusammenarbeit zu besprechen. Auf deren Rat hin hat das Unternehmen den Beweistext und den Lean-Beweis aber direkt veröffentlicht. So können Forschende selbst entscheiden, wie sie das Ergebnis prüfen.
OpenAI sieht den Beginn einer mathematisch strengen Quantenfeldtheorie
Das Physik-Ergebnis betrifft das Fundament der Teilchenphysik. Physiker beschreiben Elementarteilchen und die Kräfte zwischen ihnen mit der Quantenfeldtheorie, laut OpenAI dem wichtigsten Rahmen der modernen theoretischen Physik. Ihre Vorhersagen sind sehr genau, mathematisch exakt begründet sind die Theorien aber nicht.
Stattdessen rechnen Physiker mit Näherungen, etwa auf einem gedachten Gitter aus Punkten, das sie immer feiner machen. Offen ist, ob dabei eine eindeutige, widerspruchsfreie Theorie herauskommt, also ob eine Theorie im mathematischen Sinne "existiert". Ob sie die Natur richtig beschreibt, ist eine andere Frage.
Laut OpenAI habe die KI bewiesen, dass bestimmte Quantenfeldtheorien in vier Dimensionen existieren, also in drei Raumdimensionen und der Zeit. Ein solcher Beweis ist für Theorien, in denen Teilchen aufeinander einwirken, in vier Dimensionen bislang niemandem gelungen.
Im Zentrum steht die starke Kraft. Sie hält Quarks zu Protonen und Neutronen zusammen und sorgt damit auch für den Zusammenhalt der Atomkerne. Übertragen wird sie von Teilchen namens Gluonen. Der Beweis umfasst drei Theorien, die wie Stufen aufeinander aufbauen.
Die unterste Stufe ist die Yang-Mills-Theorie. Sie beschreibt nur die Gluonen, ohne Quarks. Zu dieser Theorie gehört eines der sieben Millennium-Preisprobleme, für die das Clay Mathematics Institute je eine Million US-Dollar ausgelobt hat.
Das Problem besteht aus zwei Teilen. Erstens soll man beweisen, dass die Yang-Mills-Theorie mathematisch existiert. Zweitens soll man zeigen, dass sie eine sogenannte Massenlücke hat. OpenAI spricht ausdrücklich nur davon, einen Teil des Problems gelöst zu haben, nämlich die Existenz. Vollständig gelöst wäre das Millennium-Problem damit also nicht.
Hinter der Massenlücke steckt ein Rätsel: In den Gleichungen haben Gluonen keine Masse. Kräfte mit masselosen Überträgern reichen normalerweise sehr weit, so wie die elektromagnetische Kraft, die vom masselosen Licht übertragen wird. Die starke Kraft wirkt dagegen nur auf winzige Entfernungen, etwa innerhalb eines Atomkerns. Physiker erklären das damit, dass sich Gluonen zu Gebilden zusammenballen, die Masse haben. Selbst das leichteste davon ist nicht masselos. Diesen Abstand zwischen null und der kleinsten möglichen Masse nennt man Massenlücke. Computersimulationen sprechen dafür, mathematisch bewiesen ist sie bisher nicht.
Die zweite Stufe ist die Quantenchromodynamik (QCD). Sie nimmt die Quarks hinzu und beschreibt die starke Kraft damit vollständig.
Dass beide Theorien mathematisch existieren können, liegt laut OpenAI vor allem an der sogenannten asymptotischen Freiheit. Gemeint ist, dass die starke Kraft schwächer wird, je näher sich die Teilchen kommen. Dadurch bleibt die Rechnung auch auf einem immer feineren Gitter beherrschbar.
Die dritte Stufe wäre eigentlich das Standardmodell der Teilchenphysik. Es beschreibt drei der vier Grundkräfte, alle außer der Schwerkraft. Laut OpenAI lasse es sich aber nicht auf beliebig kleine Abstände übertragen. Denn manche seiner Kräfte werden bei kleinen Abständen nicht schwächer, sondern stärker.
Deshalb beziehe sich der Beweis auf die einfachste sogenannte große vereinheitlichte Theorie. Sie führt die drei Kräfte auf eine einzige zurück und enthält die Kraft- und Materieteilchen des Standardmodells. Diese vereinheitlichte Kraft kann, ähnlich wie die starke Kraft, bei kleinen Abständen schwächer werden. Experimentell bestätigt sind solche Theorien allerdings nicht.
Hält der Beweis, wären alle drei Stufen mathematisch begründet. An den Vorhersagen der Physik würde das nichts ändern. OpenAI hofft aber, dass die Quantenfeldtheorie dadurch zu einem mathematisch strengen Fach wird.
Eine Gruppe um David Gross soll die Arbeit begleiten. Gross erhielt 2004 einen Anteil am Physik-Nobelpreis für seine Arbeiten zur asymptotischen Freiheit. Zur Gruppe gehören Michael Douglas, Arthur Jaffe, Igor Klebanov und Nikita Nekrasov. Jaffe hat das Millennium-Preisproblem zur Yang-Mills-Theorie mitformuliert.
Den Beweis zur Yang-Mills-Theorie hat OpenAI nach eigenen Angaben bereits in Lean übertragen. Anders als in der Informatik hält die Gruppe die Unterlagen der KI aber vorerst zurück und will das Ergebnis selbst aufschreiben.
Das Verfahren wirft eigene Fragen auf
OpenAI räumt selbst ein, dass das Verfahren Zielkonflikte mit sich bringt. Wer die ersten Hirten auswähle, bestimme mit, wer sich zuerst beteilige. Manche wüssten dadurch früher mehr als andere. Welcher der drei Wege am besten funktioniere, wisse man noch nicht.
OpenAI beansprucht nach eigenen Angaben keine wissenschaftliche Anerkennung für die Entdeckungen. Anerkennung sollen stattdessen die Gruppen bekommen, die die Ergebnisse erklären. Das Unternehmen reagiert damit offenbar auf die Kritik nach dem PR-Desaster um Navier-Stokes.
Zudem hat OpenAI fünf Millionen US-Dollar an die Simons Foundation zugesagt. Damit soll die Stiftung Workshops und Konferenzen zu KI-Ergebnissen fördern.
Über die Prüfung hinaus lädt die Gruppe um Williams in ihrem offenen Brief zu einer grundsätzlichen Debatte ein. Es soll darum gehen, wie man Durchbrüche einer KI überprüft, wer Zugang zu ihnen erhält und wem die Anerkennung gebührt.
