Der OpenAI Navier-Stokes-Beweis könnte ein Jahrhundertproblem der Mathematik lösen – und gleichzeitig zeigen, dass ein korrekter Beweis allein nicht mehr genügt. OpenAI hat eine analytische Ausarbeitung und eine formale Lean-Version veröffentlicht. Parallel erhebt der Mathematiker Tristan Buckmaster schwere Vorwürfe zur Vorgeschichte, zur Zuschreibung und zum Umgang mit privaten Forschungsdaten. Beides muss getrennt geprüft werden.
Die spektakuläre Schlagzeile lautet: Eine unveröffentlichte KI, laut OpenAI deutlich leistungsfähiger als GPT-6 Astra, habe das Navier-Stokes-Problem gelöst. Die wichtigere Geschichte dahinter lautet jedoch: Wissenschaft braucht für KI-generierte Entdeckungen künftig zwei Beweisketten – eine für die Mathematik und eine für die Herkunft der Ideen.
Was OpenAI tatsächlich behauptet
Die Navier-Stokes-Gleichungen beschreiben, wie sich Flüssigkeiten und Gase bewegen. Sie stecken unter anderem in Modellen für Flugzeugströmungen, Wetter und Blutfluss. Offen war, ob eine anfangs glatte dreidimensionale Strömung unter den Gleichungen immer glatt bleibt oder in endlicher Zeit eine Singularität entwickeln kann.
OpenAI behauptet nun, ein zunächst ruhendes Fluid mit glatter äußerer Kraft konstruiert zu haben, dessen Geschwindigkeit in endlicher Zeit unbeschränkt wächst, während die Energie endlich bleibt. Der beschriebene Wirbel zieht sich nach innen zusammen und streckt sich zugleich entlang seiner Achse. Damit sollen die Varianten C und D der offiziellen Problemstellung erfüllt sein.
Das Detail mit der äußeren Kraft ist kein Schlupfloch. Die offizielle Formulierung des Clay Mathematics Institute erlaubt bei den Negativvarianten C und D eine glatte Kraft unter präzisen Bedingungen. Die Herausforderung besteht darin, dass die Singularität aus der Strömungsdynamik entsteht und nicht durch eine bereits singuläre Kraft hineingeschmuggelt wird.
OpenAI beziffert den Aufwand auf rund 10.000 gleichzeitig arbeitende Agenten. Nach etwa 88 Stunden sei die Lösung gefunden worden. Für den Navier-Stokes-Lauf nennt das Unternehmen 2,7 Millionen Agentennachrichten und ungefähr 130 Milliarden Ausgabetoken. Die Lean-Formalisierung habe weitere 17 Stunden benötigt.
Der Unterschied zwischen Veröffentlichung und Bestätigung
OpenAI hat mehr vorgelegt als eine Pressemitteilung. Das Unternehmen veröffentlichte die Ausarbeitung und ein öffentliches Repository mit Lean-4-Zertifikaten. Das ist ein starkes Signal. Es ist aber noch nicht dasselbe wie eine allgemein akzeptierte Lösung.
Zum Zeitpunkt dieser Veröffentlichung führt das Clay Mathematics Institute das Problem weiterhin als ungelöst. Das ist normal. Bei einem Millennium-Problem prüfen Fachleute nicht nur einzelne Rechenschritte. Sie müssen auch bestätigen, dass die formalisierte Aussage exakt die offizielle Problemstellung trifft, dass alle Definitionen korrekt modelliert sind und dass kein entscheidender Zusammenhang zwischen Papier und Formalisierung verloren ging.
Lean beantwortet die Frage: Folgt der formalisierte Satz aus den verwendeten Axiomen und Definitionen? Lean beantwortet nicht automatisch, ob die Definitionen die beabsichtigte Mathematik vollständig abbilden. Noch weniger beantwortet es, woher die entscheidende Idee kam und wem dafür wissenschaftlicher Kredit zusteht.
Genau diese Grenze habe ich bereits bei KI-Beweisen beschrieben, die formal prüfbar, aber für Menschen kaum nachvollziehbar sind. Beim Navier-Stokes-Fall kommt nun eine zweite Blackbox hinzu: nicht nur der Denkweg, sondern auch die Provenienz.
OpenAI Navier-Stokes-Beweis: drei Prüfungen statt eines grünen Hakens
Der Fall lässt sich nicht mit einem einzigen Urteil „bewiesen“ oder „unbewiesen“ sauber erfassen. Ich würde drei voneinander unabhängige Prüfungen verlangen.
1. Formale Gültigkeit
Baut der Lean-Code ohne Lücken? Sind keine unbewiesenen Platzhalter enthalten? Stimmen Axiome, Definitionen und Hauptsatz? Diese Ebene ist maschinell prüfbar und deshalb die stärkste Seite der Veröffentlichung.
2. Mathematische Bedeutung
Entspricht der formale Hauptsatz wirklich den Varianten C und D? Erfüllt die Kraft alle verlangten Glattheits- und Abklingbedingungen? Ist die analytische Konstruktion für unabhängige Fachleute verständlich und reproduzierbar? Hier beginnt klassische Begutachtung. Ein kompilierendes Zertifikat ersetzt sie nicht, sondern macht sie präziser.
3. Wissenschaftliche Provenienz
Welche Literatur, Prompts, Zwischenergebnisse und menschlichen Eingriffe führten zur Lösung? Welche unveröffentlichten Daten konnten in Training oder Modellverbesserung eingeflossen sein? Wer entwickelte die tragende Forschungsrichtung? Diese Fragen liegen außerhalb des Lean-Kernels. Trotzdem entscheiden sie über Vertrauen und Zuschreibung.
Das ist die zentrale Lehre: Mathematische Korrektheit und wissenschaftliche Redlichkeit sind zwei verschiedene Eigenschaften. Ein Resultat kann korrekt sein und trotzdem eine ungeklärte Entstehungsgeschichte haben. Umgekehrt beweist ein hässlicher Streit nicht, dass der mathematische Satz falsch ist.
Worum es im Streit mit Buckmaster und Alpöge geht
Tristan Buckmaster von der New York University und Levent Alpöge, Mitarbeiter bei Anthropic, arbeiteten nach Buckmasters Darstellung etwa ein Jahr an verwandten Blow-up-Problemen. Sie nutzten dabei mehrere Sprachmodelle, darunter Claude und OpenAI-Systeme. Ihre veröffentlichten Resultate betreffen unter anderem die Euler-Gleichungen mit glatter äußerer Kraft – eine verwandte, aber andere Aussage als OpenAIs Navier-Stokes-Resultat.
In seiner öffentlichen Stellungnahme betont Buckmaster selbst, dass er OpenAIs Beweis vor dessen Veröffentlichung nicht gesehen habe und nicht wisse, ob gemeinsame Daten verwendet wurden. Gleichzeitig beschreibt er mehrere konkrete Gründe für sein Misstrauen. Die Route über glatte äußere Kräfte sei ungewöhnlich und entspreche genau dem Forschungsprogramm, an dem er und Alpöge arbeiteten. Außerdem hätten ihre privaten Codex-Sitzungen Entwürfe des Projekts enthalten.
Buckmaster wirft OpenAI ferner vor, Fragen zum Training nicht klar beantwortet und bei Gesprächen über Veröffentlichung und Autorenschaft Druck ausgeübt zu haben. Sébastien Bubeck weist die Darstellung als falsch und aufrührerisch zurück. OpenAI erklärt, weder Menschen noch Agenten hätten vor der Veröffentlichung auf die Arbeit der beiden Forscher zugegriffen. Das Unternehmen räumt zugleich ein, nicht vollständig ausschließen zu können, dass anonymisierte Daten aus ihrer Produktnutzung zur Modellverbesserung beitrugen.
Die WIRED-Recherche, die diesen Beitrag angestoßen hat, beschreibt deshalb zu Recht zwei Geschichten zugleich: einen möglichen mathematischen Durchbruch und einen eskalierenden Prioritätskonflikt. Die Vorwürfe sind derzeit nicht unabhängig belegt. Sie einfach als Nebengeräusch abzutun wäre dennoch ein Fehler.
Warum „Lean-verifiziert“ den Herkunftsstreit nicht löst
In Softwarebegriffen ist Lean ein sehr strenger Test für eine spezifizierte Eigenschaft. Es ist kein Audit-Log für den Entwicklungsprozess. Ein grüner Build sagt nichts darüber aus, ob Code aus einem privaten Repository übernommen, eine Idee korrekt zugeschrieben oder ein Datensatz vertragsgemäß verwendet wurde.
Genau deshalb greift die Debatte über unverständliche Beweise zu kurz. Mein früherer Beitrag zur Leiden Declaration und ihren Warnungen vor fehlender Zuschreibung klang im Juni noch wie eine Governance-Debatte für die Zukunft. Der Navier-Stokes-Fall macht daraus eine aktuelle Infrastrukturfrage.
Wer KI-Forschung nur auf Ergebnisqualität prüft, baut ein System mit perfekter Endkontrolle und blinder Lieferkette. Für wissenschaftliche Erkenntnisse ist das nicht genug.
Was Forschungsteams jetzt protokollieren sollten
Die Antwort kann nicht lauten, private Forschung grundsätzlich von KI-Systemen fernzuhalten. Dafür ist der Produktivitätsgewinn zu groß. Aber Teams brauchen einen nachvollziehbaren Herkunftsnachweis, bevor ein Konflikt entsteht.
- Prompts und Modellversionen unveränderlich protokollieren. Zu jedem Lauf gehören Zeitpunkt, Modell, Werkzeuge, bereitgestellte Quellen und relevante Systemeinstellungen.
- Trainings- und Nutzungsbedingungen projektbezogen festhalten. Ein späterer Verweis auf eine allgemeine Datenschutzseite reicht bei unveröffentlichter Forschung nicht. Die konkrete Datenklasse und das vereinbarte Training-Opt-out gehören ins Projektprotokoll.
- Ideenherkunft von Textähnlichkeit trennen. Wissenschaftlicher Kredit hängt oft an einer Strategie oder Problemreduktion, nicht an identischen Sätzen. Das Ledger muss festhalten, wann eine Richtung erstmals auftauchte und welche Quelle sie auslöste.
- Formale Beweise und Entstehungsprotokolle gemeinsam veröffentlichen. Das Lean-Zertifikat prüft die Logik. Ein Provenienzbericht erklärt Datenzugriff, menschliche Eingriffe, Suchraum und Vorarbeiten.
- Unabhängige Prüfer für beide Ebenen benennen. Mathematiker prüfen den Satz. Daten- und Forschungsintegritätsprüfer untersuchen die Entstehung. Ein Team sollte nicht sein eigener Gutachter sein.
Diese Trennung ist auch für Unternehmen nützlich. Wer KI-generierten Code, Patente oder Strategien übernimmt, braucht nicht nur funktionale Tests. Er braucht eine belastbare Antwort auf die Frage, aus welchen Daten und Vorarbeiten das Ergebnis entstand.
Die unbequeme These: Der Engpass ist nicht mehr die Idee
Der erstaunlichste Teil der OpenAI-Ankündigung ist nicht, dass eine KI einen langen Beweis schreiben kann. Es ist die industrielle Suchmaschine dahinter: Tausende Agenten verfolgen parallel unterschiedliche Varianten, tauschen Zwischenergebnisse aus und werden während des Laufs auf ein verbessertes Modell umgestellt.
Damit verschiebt sich der Engpass. Knapp sind nicht mehr nur mathematische Einfälle. Knapp werden Rechenbudget, kuratierter Zugang zur Literatur, formale Verifikation und glaubwürdige Provenienz. Ein Labor mit Millionenbudget kann einen Forschungsraum in Tagen abdecken, für den kleine Gruppen Jahre benötigen.
Das ist kein Argument gegen KI-gestützte Mathematik. Es ist ein Argument gegen die naive Vorstellung, wissenschaftliche Fairness entstehe automatisch, sobald der finale Beweis öffentlich ist. Die Entwicklung von KI als mathematischem Forschungsassistenten erreicht gerade den Punkt, an dem technische Leistungsfähigkeit schneller wächst als die Regeln für Kredit, Daten und Veröffentlichung.
Fazit: Zwei Beweisketten für eine neue Wissenschaft
Der OpenAI Navier-Stokes-Beweis kann mathematisch korrekt sein. Die öffentliche Lean-Formalisierung macht die Behauptung deutlich ernster als eine normale Produktankündigung. Ob das Millennium-Problem tatsächlich gelöst ist, müssen unabhängige Fachleute und letztlich die mathematische Gemeinschaft entscheiden.
Der Prioritäts- und Datenstreit läuft auf einer anderen Achse. Buckmasters Vorwürfe sind keine bewiesenen Tatsachen. OpenAIs Dementi ist aber ebenfalls kein unabhängiges Audit. Wer beide Fragen vermischt, macht es sich zu leicht.
Mein Urteil ist deshalb vorläufig, aber klar: Die Mathematik verdient eine gründliche Prüfung ohne Vorverurteilung. Die Entstehungsgeschichte verdient dieselbe Strenge. In einer Welt maschinell erzeugter Forschung brauchen wir künftig nicht nur den Beweis, dass ein Satz stimmt. Wir brauchen auch den Beweis, dass wir wissen, wie er entstanden ist.
