OpenAI legt formalen Beweis für Navier-Stokes vor
OpenAI hat am 8. September 2026 eine angebliche Lösung des Navier-Stokes-Millennium-Problems veröffentlicht. Nach Darstellung des Unternehmens zeigt der Beweis, dass die Strömung eines dreidimensionalen Fluids trotz glatter Anfangsbedingungen in endlicher Zeit eine Singularität entwickeln kann.
Eine Singularität bezeichnet in diesem Zusammenhang einen mathematischen Zustand, bei dem die Geschwindigkeit innerhalb endlicher Zeit unbegrenzt wächst. OpenAI beansprucht damit, die Aussagen C und D der offiziellen Problemdefinition bewiesen zu haben.
Sinngemäß erklärt OpenAI: „Dieser von einem internen OpenAI-System erstellte Beweis zeigt, dass die Dynamik der Navier-Stokes-Gleichungen für Flüssigkeitsbewegungen in endlicher Zeit eine Singularität entwickeln kann.“
Die entscheidende Einschränkung lautet: Eine unabhängige Begutachtung und Anerkennung durch die internationale Mathematikgemeinschaft oder das Clay Mathematics Institute ist bislang nicht bestätigt. Der veröffentlichte Beweis ist daher zunächst eine Behauptung von OpenAI, wenn auch eine ungewöhnlich detailliert und formal dokumentierte.
Worum es beim Navier-Stokes-Problem geht
Die Navier-Stokes-Gleichungen beschreiben die Bewegung von Flüssigkeiten und Gasen als kontinuierliches Medium. Sie werden unter anderem bei der Entwicklung von Flugzeugen, in Wettermodellen und bei der Untersuchung von Blutströmungen eingesetzt.
Offen war seit den Arbeiten von Jean Leray aus dem Jahr 1934, ob glatte Lösungen für dreidimensionale Strömungen immer glatt bleiben. OpenAI beschreibt nun eine Wirbelstruktur, die sich nach innen bewegt, zunehmend gestreckt wird und dabei immer schneller rotiert. Die Energie soll dennoch während des gesamten Vorgangs endlich bleiben.
Der mathematisch schwierige Teil liegt laut OpenAI im präzisen Zusammenspiel von Beschleunigung, Druckgradienten, Impulsübertragung und Viskosität. Diese Terme sollen stark anwachsen, sich aber so ausgleichen, dass die von außen wirkende Kraft glatt bleibt.
10.000 KI-Agenten arbeiteten parallel
Der Beweis entstand nicht in einer einzelnen Modellausgabe. OpenAI setzte ein koordiniertes Multi-Agenten-System ein, bei dem viele Modellinstanzen parallel unterschiedliche Ansätze verfolgen und Zwischenergebnisse austauschen.
Die erfolgreiche Gruppe umfasste nach Unternehmensangaben rund 10.000 gleichzeitig aktive Agenten. Sie konnten auf einen zwischengespeicherten Ausschnitt des Internets zugreifen und Code ausführen. Codex bündelte relevante Zwischenergebnisse und führte sie anderen Gruppen als zusätzlichen Kontext zu.
Als Grundlage diente ein unveröffentlichtes internes Modell, dessen Training laut OpenAI am 28. August 2026 begann. Das Unternehmen bezeichnet es als deutlich leistungsfähiger als GPT-6 Astra. Technische Details zur Infrastruktur und Architektur nennt OpenAI nicht.
| Schritt | Aufwand laut OpenAI |
|---|---|
| Vorangehende Lösung zum Euler-Regularitätsproblem | Knapp 100 Agenten, rund 50 Stunden |
| Suche nach der Navier-Stokes-Lösung | Rund 10.000 parallele Agenten, etwa 88 Stunden |
| Navier-Stokes-Ressourcen | 2,7 Millionen Nachrichten, rund 130 Milliarden Output-Tokens |
| Lean-Formalisierung und Verifikation | Weitere 17 Stunden mit GPT-6 Astra |
| Gesamtes Projekt über alle untersuchten Probleme | 4,9 Millionen Nachrichten, rund 300 Milliarden Output-Tokens |
Das Projekt startete am 1. September 2026. Am 5. September erreichten die Agenten laut OpenAI nach etwa 88 Stunden die entscheidende Lösung. Zuvor hatte eine kleinere Gruppe ein Regularitätsproblem für die unbeeinflussten Euler-Gleichungen bearbeitet, also eine verwandte Gleichung ohne Viskosität und äußere Kraft.
Der Umfang geht weit über übliche Agentenprojekte hinaus. Zum Vergleich zeigen auch veröffentlichte Messungen zu OpenAIs Agenten-Arbeitstagen in der Forschung, dass der Anbieter wissenschaftliche Arbeit zunehmend als skalierbaren Rechenprozess behandelt.
Lean macht den Beweis maschinell prüfbar
Nach der Lösungsfindung wurde der Beweis mit GPT-6 Astra in Lean formalisiert. Lean ist ein interaktiver Beweisassistent, der jeden logischen Schritt anhand eines kleinen, deterministischen Prüfkerns kontrolliert.
Damit hängt die technische Überprüfung nicht allein vom Urteil des generierenden Modells ab. Fehler in der formalen Ableitung würden vom Prüfsystem zurückgewiesen. Einen ähnlichen Ansatz nutzte Anthropic bei der Formalisierung eines Fermat-Beweises in Lean.
Eine erfolgreiche Lean-Prüfung ersetzt allerdings nicht jede wissenschaftliche Kontrolle. Fachleute müssen weiterhin untersuchen, ob die Formalisierung tatsächlich die offizielle Aufgabenstellung trifft, ob alle Annahmen zulässig sind und ob die mathematische Konstruktion korrekt interpretiert wurde.
Ressourcenbedarf schafft neue Abhängigkeiten
Die veröffentlichten Verbrauchswerte zeigen die wirtschaftliche Grenze dieses Ansatzes. Rund 130 Milliarden Output-Tokens und 10.000 parallele Agenten lassen sich nicht mit einem gewöhnlichen KI-Abonnement abbilden. OpenAI nennt weder die Betriebskosten noch die benötigte Recheninfrastruktur.
Für Unternehmen entsteht damit eine starke Abhängigkeit von proprietären Spitzenmodellen und Hyperscaler-Ressourcen. Eigene Reproduktion ist ohne vergleichbare Infrastruktur kaum möglich. Gleichzeitig liefert die formale Verifikation ein Gegenmodell zur reinen Anbieterabhängigkeit, weil das Ergebnis mit offenen und deterministischen Werkzeugen unabhängig geprüft werden kann.
Für forschungsintensive Branchen im DACH-Raum, etwa Automobilbau, Luftfahrt und Strömungssimulation, liegt die unmittelbare Bedeutung weniger in einer kurzfristigen Produktfunktion. Relevant ist vielmehr die demonstrierte Methode: Viele spezialisierte Agenten untersuchen parallel ein Problem, während ein formales System die belastbaren Resultate absichert.
OpenAI erklärt, das Preisgeld für das Millennium-Problem nicht beanspruchen zu wollen. Ob der Beweis tatsächlich als Lösung eines der sieben Millennium-Probleme anerkannt wird, entscheidet sich jedoch erst durch die unabhängige mathematische Prüfung.