OpenAIs Navier-Stokes-Beweis: Fachleute sehen einen anderen Lösungsweg

Lean-Prüfung und verständliche Darstellung sind nicht dasselbe

OpenAI veröffentlichte neben dem schriftlichen Beweis eine Formalisierung in Lean. Diese Programmiersprache erlaubt es, logische Schritte so auszudrücken, dass ein formales System sie überprüfen kann. Die Formalisierung kann dadurch eine andere Art von Prüfung ermöglichen als die Lektüre eines langen mathematischen Textes. [1] [2] [3]

Das löst jedoch nicht jede Frage, die an einen veröffentlichten Beweis gestellt wird. Eine formale Prüfung betrifft die in Lean kodierte Argumentation und die darin formulierte Aussage. Sie ersetzt nicht automatisch die fachliche Einordnung, wie diese Formalisierung mit der begleitenden Darstellung zusammenhängt oder ob die beschriebene Methode neu ist. Diese Fragen sind Teil der laufenden Auswertung durch Mathematiker. [1] [3]

Scientific American berichtet, dass mehrere Forschungsgruppen sowohl den Lean-Code als auch den Text untersuchen und dabei weitere Sprachmodelle zur Orientierung einsetzen. Der Beitrag beschreibt den Beweis als schwer lesbar, selbst für ausgewiesene Fachleute. Aus den vorliegenden Berichten geht aber nicht hervor, dass die Lean-Prüfung gescheitert wäre oder die formale Aussage widerlegt wurde. [3]

Das Clay Mathematics Institute prüfte den Beweis nach Angaben von The Decoder seit seiner Veröffentlichung. Zum Stand der Berichte vom 17. Oktober lag dort noch kein mitgeteiltes abschließendes Urteil vor. OpenAI erklärte seinerseits, mit der Veröffentlichung keinen Anspruch auf den Millennium-Preis erheben zu wollen. [1] [2]

Die Herkunft lässt sich nicht vollständig rekonstruieren

OpenAI erklärte nach einer internen Untersuchung, Buckmasters Codex-Eingaben aus den zwei Monaten vor der Veröffentlichung hätten das interne Modell nicht beeinflusst – auch nicht über das Training. Das Unternehmen beschrieb das verwendete Modell als ein zuvor vortrainiertes System, das anschließend mit umfangreichem Reinforcement Learning weiterentwickelt worden sei. [2]

Scientific American gibt OpenAIs Dementi wieder, verweist aber zugleich auf die Black-Box-Eigenschaften großer Sprachmodelle. Camillo De Lellis vom Institute for Advanced Study wird dort mit der Einschätzung zitiert, eine abschließende Tatsachenklärung zum konkreten Gedankengang sei vermutlich nicht möglich. Das ist keine Bestätigung eines unzulässigen Einflusses, sondern eine Aussage über die Grenzen nachträglicher Rekonstruktion. [3]

OpenAI berichtete außerdem, es habe nach Abschluss des Projekts Kontakt zu Buckmaster und Alpöge aufgenommen und ihnen Einsicht in verwendete Prompts sowie später in den Beweis angeboten. Das Unternehmen erklärte, die eigene Arbeit unterscheide sich von ihrer Lösung zur Euler-Gleichung auch darin, dass deren Ergebnis eine äußere Kraft einbezog, während OpenAIs Variante ohne äußere Kraft auskam. [2]

Die verfügbaren Quellen erlauben damit eine Einordnung der publizierten Methoden und der konkurrierenden Aussagen, aber keine vollständige Rekonstruktion sämtlicher Einflüsse auf die internen Agenten. Die Frage nach wissenschaftlicher Priorität und die Frage nach der formalen Gültigkeit eines Beweises sind dabei getrennt zu behandeln. [2] [3]

Ein großer Agentenschwarm, aber kein belastbarer Vergleich

OpenAI zufolge arbeiteten die Agenten rund 88 Stunden an der Navier-Stokes-Lösung; anschließend benötigten Formalisierung und Überprüfung in Lean weitere 17 Stunden. Die Gruppe, die den Beweis hervorbrachte, umfasste nach Unternehmensangaben etwa 10.000 gleichzeitig aktive Agenten. Für den gesamten Navier-Stokes-Versuch nennt OpenAI 2,7 Millionen Nachrichten und ungefähr 130 Milliarden ausgegebene Tokens. [2]

Die Größenordnung belegt, dass die Lösung mit erheblichem Rechen- und Koordinationsaufwand entstand. Sie zeigt für sich genommen aber nicht, welcher Teil des Ergebnisses auf die Anzahl der Agenten, auf das zugrunde liegende Modell oder auf die Organisation der Arbeit zurückzuführen ist. OpenAI-Forscher Noam Brown schätzte laut The Decoder den Anteil des Multi-Agenten-Setups am Erfolg auf weniger als zehn Prozent. [1]

Brown zufolge sei vor allem die Fähigkeit des Basismodells wichtig gewesen, über längere Zeit an Aufgaben zu arbeiten und Prozesse parallel auszuführen. Zugleich gebe es keine systematischen Vergleichstests dazu, wie lange ein einzelner Agent für dieselbe Aufgabe benötigt hätte. Auch der konkrete Vorteil von 10.000 gegenüber 1.000 Agenten sei nach den vorliegenden Angaben nicht ermittelt worden; solche Versuche seien zu teuer. [1]

Für Unternehmen folgt daraus keine allgemeine Aussage gegen Agentensysteme. Die engere Schlussfolgerung lautet: Ein spektakuläres Ergebnis unter hoher Parallelisierung ist kein Nachweis, dass die gewählte Agentenzahl wirtschaftlich optimal oder gegenüber kleineren Konfigurationen überlegen ist. Dafür wären kontrollierte Vergleiche nötig, die in diesem Fall laut den Berichten fehlen. [1]

Was Unternehmen aus dem Fall ableiten können

Der Fall macht sichtbar, dass bei KI-gestützter Forschung mehrere Erfolgskriterien auseinanderfallen können: Ein System kann ein formal prüfbares Resultat erzeugen, während Fachleute noch die verständliche Darstellung, den konkreten Lösungsweg und die wissenschaftliche Einordnung untersuchen. Die Quellen belegen hier eine laufende fachliche Prüfung, nicht ein abschließendes Urteil über sämtliche Aspekte des OpenAI-Beweises. [1] [3]

Für den Einsatz solcher Systeme in Forschung und Entwicklung ist deshalb nicht nur das Endergebnis relevant. Ebenso wichtig ist, ob sich Zwischenschritte, Modellversionen, Eingaben und Übergänge zwischen informeller Argumentation und formaler Prüfung nachvollziehen lassen. Das ist eine Analyse der Anforderungen, die sich aus den dokumentierten Unsicherheiten ergeben; die verfügbaren Berichte belegen nicht, in welchem Umfang OpenAI intern sämtliche dieser Informationen protokolliert hat. [1] [2] [3]

Auch die Kostenfrage bleibt offen. Bei rund 130 Milliarden Tokens für den Navier-Stokes-Versuch lässt sich der Aufwand nicht sinnvoll allein anhand des Resultats bewerten, solange Vergleichswerte für kleinere Agentengruppen oder einzelne Modelle fehlen. Unternehmen, die parallele KI-Systeme evaluieren, sollten den beobachteten Nutzen daher nicht mit der bloßen Zahl eingesetzter Agenten gleichsetzen. [1] [2]

Die zentrale Nachricht ist somit weder eine bestätigte Widerlegung noch eine uneingeschränkte Bestätigung von OpenAIs ursprünglicher Darstellung. Fachleute erkennen im endgültigen Beweis einen anderen Lösungsweg als den zunächst vermuteten; die formale und mathematische Prüfung läuft weiter, während die genaue Entstehungsgeschichte des Ergebnisses nur begrenzt rekonstruierbar bleibt. [1] [3]

Quellen

1. [1] Mathematicians say OpenAI doesn't understand its own Navier-Stokes proof — https://the-decoder.com/mathematicians-say-openai-doesnt-understand-its-own-navier-stokes-proof (abgerufen am 2026-10-17)
2. [2] On the Navier–Stokes Millennium Prize Problem | OpenAI — https://openai.com/index/navier-stokes-solution (abgerufen am 2026-10-17)
3. [3] OpenAI’s blockbuster Navier-Stokes proof isn’t what we thought it was | Scientific American — https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was (abgerufen am 2026-10-17)