OpenAI legt KI-Beweis zu Navier-Stokes vor: Was jetzt wirklich bestätigt ist

Was OpenAI am 8. September veröffentlicht hat

OpenAI stellt einen analytischen Beweis mit dem Titel Finite Time Blowup for Navier-Stokes bereit. Hinzu kommt ein öffentliches GitHub-Repository mit Lean-4-Formalisationen für Navier-Stokes und die verwandten Euler-Gleichungen. Damit ist die Behauptung nicht nur in einer Produktmeldung beschrieben: Paper, formale Zertifikate und Bauanleitung für die Lean-Prüfung können von Fachleuten untersucht werden.

Der zentrale Satz betrifft die dreidimensionalen inkompressiblen Navier-Stokes-Gleichungen mit positiver Viskosität. OpenAI konstruiert nach eigener Darstellung eine glatte, räumlich und zeitlich kompakt getragene äußere Kraft sowie eine anfangs ruhende Strömung. Deren Geschwindigkeit wird innerhalb endlicher Zeit unbeschränkt, während die kinetische Energie gleichmäßig beschränkt bleibt.

Ereignisdatum: 8. September 2026. Bestätigt ist die Veröffentlichung eines Papers und von Lean-Code. Ob der Beweis mathematisch vollständig und die behauptete Lösung allgemein anerkannt ist, wird erst unabhängig geprüft.

Worum es beim Navier-Stokes-Problem geht

Die Navier-Stokes-Gleichungen beschreiben die Bewegung von Flüssigkeiten und Gasen, etwa Wasserströmungen oder Luft. Im dreidimensionalen Fall ist seit Jahrzehnten offen, ob eine zunächst glatte Strömung unter den geforderten Bedingungen immer glatt bleibt oder in endlicher Zeit eine Singularität entwickeln kann. Vereinfacht gesagt geht es darum, ob mathematische Größen wie die Geschwindigkeit trotz Viskosität ohne Grenze anwachsen können.

Das Clay Mathematics Institute nahm die Existenz- und Glattheitsfrage im Jahr 2000 in seine sieben Millennium-Probleme auf. Die offizielle Formulierung lässt mehrere Lösungswege zu. OpenAIs Arbeit zielt auf die Alternativen C und D: den Zusammenbruch einer Lösung im ganzen Raum beziehungsweise auf einem periodischen dreidimensionalen Torus.

Welche Konstruktion das Paper behauptet

Der Lösungsvorschlag baut einen sich zusammenziehenden Wirbel auf. Während sein Kern schmaler wird, nehmen Dreh- und Axialgeschwindigkeit zu. Räumlich oszillierende Impulse sollen die sonst singulären Restterme so ausgleichen, dass die von außen angelegte Kraft selbst glatt bleibt. Die Strömung wird lokal immer schneller, ohne dass ihre gesamte kinetische Energie unbeschränkt wächst.

Dieser Unterschied ist wesentlich: Für eine frei gewählte Geschwindigkeit könnte man die Gleichung formal immer durch eine passend definierte Kraft erfüllen. Die mathematische Schwierigkeit besteht darin, zugleich den Blow-up der Geschwindigkeit, endliche Energie, Inkompressibilität und eine glatte Kraft mit den verlangten Trägereigenschaften nachzuweisen. Genau diese Abschätzungen füllen den größten Teil des 166-seitigen Papers.

OpenAI beansprucht eine Konstruktion mit glatter äußerer Kraft. Das ist nicht dasselbe wie ein Beweis für einen Blow-up der vollständig ungestörten Navier-Stokes-Gleichungen ohne äußere Kraft.

Was die Lean-Formalisation leistet und was nicht

Lean ist ein interaktiver Theorembeweiser. Ein erfolgreich geprüftes Lean-Projekt zeigt, dass die formal kodierten Schlussfolgerungen aus den formal kodierten Definitionen, Annahmen und Hilfssätzen folgen. Das reduziert das Risiko vieler klassischer Rechen- und Logikfehler erheblich und macht den Prüfpfad reproduzierbarer als eine bloße Behauptung in Prosa.

Trotzdem beantwortet ein grüner Lean-Build nicht automatisch jede wissenschaftliche Frage. Fachleute müssen prüfen, ob die formalisierten Definitionen exakt zur offiziellen Problemformulierung passen, ob die Verbindung zwischen dem analytischen Paper und dem formalen Modell vollständig ist und ob keine entscheidende Voraussetzung unbeabsichtigt abgeschwächt wurde. OpenAIs Repository stellt dafür den Code und zusätzliche Hinweise zur unabhängigen Prüfung bereit.

• Paper prüfen: Sind alle analytischen Abschätzungen und Grenzübergänge gültig?
• Spezifikation prüfen: Entspricht der formale Satz wirklich den Clay-Alternativen C und D?
• Lean-Code neu bauen: Lässt sich die Formalisation in einer unabhängigen Umgebung reproduzieren?
• Verknüpfung prüfen: Deckt der Lean-Code alle für das Paper zentralen Argumente ab?

Wie OpenAI den Beweis mit Agenten erzeugt haben will

OpenAI beschreibt ein koordiniertes System aus ungefähr 10.000 gleichzeitig arbeitenden Agenten. Gruppen erhielten verschiedene Varianten der offenen Probleme, konnten Code ausführen, auf einen zwischengespeicherten Internetbestand zugreifen und innerhalb ihrer Gruppe kommunizieren. Codex habe anschließend nützliche Zwischenergebnisse verschiedener Gruppen konsolidiert und für weitere Suchläufe verfügbar gemacht.

Nach Unternehmensangaben erreichte die Navier-Stokes-Gruppe das Ergebnis nach etwa 88 Stunden. Für diesen Teil des Projekts nennt OpenAI 2,7 Millionen Nachrichten und ungefähr 130 Milliarden Ausgabetokens. Die Lean-Formalisation und Verifikation habe weitere 17 Stunden mit GPT-6 Astra benötigt. Diese Zahlen stammen ausschließlich von OpenAI; unabhängige Messdaten über Suchverlauf, Kosten oder den Anteil menschlicher Eingriffe liegen in der Veröffentlichung nicht vollständig vor.

Herstellerangabe: Umfang, Laufzeit und Tokenzahlen des Agentensystems sind von OpenAI berichtet und bislang nicht unabhängig verifiziert.

Das beteiligte Modell ist noch nicht öffentlich verfügbar

Für die Suche nach dem analytischen Beweis verwendete OpenAI nach eigener Aussage ein internes Modell, das deutlich leistungsfähiger als GPT-6 Astra sei. Das Training laufe seit dem 28. August weiter. Ein Modellname, eine öffentliche System Card, Zugriffsmöglichkeiten, Preise oder unabhängige Benchmarks werden in der Mitteilung nicht genannt.

Aus dem veröffentlichten Ergebnis lässt sich deshalb noch kein allgemeines Leistungsniveau ableiten. Ein einzelner spektakulärer Forschungsfall sagt wenig darüber aus, wie zuverlässig das System bei anderen mathematischen Aufgaben arbeitet, wie viele erfolglose Ansätze vorausgingen oder welche menschliche Expertise in Auswahl, Prüfung und Aufbereitung eingeflossen ist.

Warum das Millennium-Problem noch nicht offiziell als gelöst gilt

Das Clay Mathematics Institute führt die Navier-Stokes-Gleichung derzeit weiterhin in der Liste der ungelösten Probleme. Das ist kein unmittelbares Urteil gegen OpenAIs Paper, sondern entspricht dem vorgeschriebenen Verfahren: Das Institut nimmt keine direkten Lösungseinreichungen an und entscheidet nicht wenige Tage nach einer Veröffentlichung.

Nach den offiziellen Regeln muss ein Lösungsvorschlag zuerst in einem qualifizierten Publikationsorgan erscheinen. Danach müssen mindestens zwei Jahre vergehen, und die Arbeit muss allgemeine Anerkennung in der weltweiten Mathematikgemeinschaft erhalten, bevor das Institut sie für den Preis berücksichtigt. OpenAI erklärt selbst, den Millennium-Preis für dieses Ergebnis nicht beanspruchen zu wollen.

Stand 10. September 2026: Clay listet Navier-Stokes weiter als ungelöst. Paper und Lean-Zertifikate sind ein prüfbarer Lösungsvorschlag, keine bereits abgeschlossene offizielle Anerkennung.

Warum der Vorgang für die KI-Entwicklung bedeutend ist

Selbst wenn die mathematische Prüfung später einen Fehler finden sollte, dokumentiert die Veröffentlichung einen neuen Maßstab für KI-gestützte Forschung: sehr viele spezialisierte Agenten, maschinelle Konsolidierung von Zwischenergebnissen, ein langes analytisches Dokument und eine formale Darstellung werden in einem gemeinsamen Prozess verbunden. Entscheidend ist nicht nur die Generierung eines Textes, sondern die Bereitstellung prüfbarer Artefakte.

Sollte der Beweis unabhängiger Prüfung standhalten, wäre die wissenschaftliche Tragweite außerordentlich. Gleichzeitig würde der Fall zeigen, dass Spitzenmodelle in klar formalisierten Disziplinen nicht nur bekannte Methoden anwenden, sondern neue, sehr lange Argumentketten entwickeln können. Der Beleg dafür ist jedoch nicht OpenAIs Selbsteinschätzung, sondern die kommende Arbeit unabhängiger Mathematiker und formaler Verifikationsgruppen.

Woran sich neue Behauptungen zum Beweis messen lassen

In den nächsten Tagen werden schnelle Kommentare, Teilprüfungen und möglicherweise widersprüchliche Einschätzungen erscheinen. Einzelne Social-Media-Posts reichen weder für eine Bestätigung noch für eine Widerlegung. Belastbar sind konkrete Verweise auf Definitionen, Lemmata, Lean-Dateien oder reproduzierbare Build-Ergebnisse.

Leser sollten außerdem zwischen vier Aussagen unterscheiden: OpenAI hat die Artefakte veröffentlicht; der Lean-Code lässt sich technisch bauen; die Formalisation bildet den beanspruchten mathematischen Satz korrekt ab; und die Mathematikgemeinschaft erkennt die Lösung allgemein an. Die erste Aussage ist belegt. Die weiteren Stufen benötigen unabhängige Prüfung und Zeit.

• Auf konkrete Seiten, Sätze oder Codepfade statt auf allgemeine Zustimmung achten
• Technische Reproduzierbarkeit und mathematische Bedeutung getrennt bewerten
• Korrekturen und Versionen des Papers sowie des Repositories dokumentieren
• Den offiziellen Status beim Clay Mathematics Institute prüfen
• Herstellerangaben zum internen Modell nicht mit unabhängigen Benchmarks verwechseln

Die MindrAils-Einordnung

OpenAIs Navier-Stokes-Veröffentlichung ist eine der bedeutendsten KI-Forschungsmeldungen des Jahres, weil sie einen überprüfbaren mathematischen Anspruch mit einem ungewöhnlich großen Agentensystem verbindet. Paper und Lean-Code machen die Arbeit wesentlich substanzieller als eine bloße Modell-Demo. Zugleich wäre es journalistisch falsch, wenige Tage nach dem Release von einer endgültig gelösten Jahrhundertfrage zu sprechen.

Der faire Status lautet: OpenAI hat einen detaillierten, formalisierten Lösungsvorschlag vorgelegt. Jetzt beginnt der Teil, den auch sehr leistungsfähige KI nicht überspringen kann: unabhängige Reproduktion, fachliche Kritik und langfristige Anerkennung. Ob daraus eine bestätigte Lösung wird, entscheidet nicht die Größe des Modells, sondern die Haltbarkeit jedes einzelnen mathematischen Schritts.