Seit dem 8. September 2026 ist eine Frage aus der mathematischen Spitzenforschung plötzlich öffentlich geworden: Hat OpenAI eines der berühmtesten ungelösten Mathematikprobleme gelöst?

OpenAI hat einen 166-seitigen Text, Finite Time Blowup for Navier–Stokes, und eine Formalisation in Lean veröffentlicht. Das Unternehmen sagt, ein internes AI-System habe damit das Navier–Stokes-Millennium-Problem gelöst.

Was ist das Navier–Stokes-Problem?

Die Navier–Stokes-Gleichungen beschreiben, wie sich Flüssigkeiten und Gase bewegen. Das Millennium-Problem fragt, ob dreidimensionale Lösungen immer glatt bleiben oder unter bestimmten Bedingungen in endlicher Zeit eine Singularität entwickeln können.

Eine Singularität heißt hier: Die mathematische Lösung erreicht einen Zustand, in dem beispielsweise die Geschwindigkeit ohne Grenze wächst. Das ist eine Aussage über das Verhalten der Gleichungen – nicht die Behauptung, dass echtes Wasser buchstäblich unendlich schnell fließt.

Was behauptet OpenAI genau?

OpenAI beschreibt eine glatte Strömung, die unter einer ebenfalls glatten äußeren Kraft in endlicher Zeit eine Singularität entwickelt, während ihre kinetische Energie beschränkt bleibt. Damit beansprucht das Paper die Alternativen C und D der offiziellen Clay-Formulierung.

Das ist wichtig, weil C und D ausdrücklich eine glatte äußere Kraft erlauben. Der pauschale Einwand „forcing zählt nicht“ trifft die offizielle Aufgabenstellung deshalb nicht. Gleichzeitig folgt daraus nicht, dass OpenAI den populäreren unforced Fall A/B gezeigt hätte.

Fünf verschiedene Ebenen

Was beweist Lean – und was nicht?

Lean ist ein Proof Assistant. Eine formalisierte Aussage wird in eine strenge mathematische Sprache übersetzt und von einem kleinen Prüfkern kontrolliert. Das hilft, logische Lücken innerhalb der Formalisation zu vermeiden.

Aber: Lean beweist nicht automatisch die Entstehungsgeschichte einer Idee, ihre Priorität, die Vollständigkeit ihrer Provenance oder die gesellschaftliche Bedeutung eines Resultats. Auch die Frage, ob die formal codierte Aussage exakt mit einer öffentlichen Kurzbeschreibung übereinstimmt, muss fachlich geprüft werden.

Warum Clay nicht am nächsten Morgen entscheidet

Die Regeln des Clay Mathematics Institute verlangen für eine mögliche Prize-Anerkennung unter anderem eine qualifizierende Publikation, mindestens zwei Jahre seit Veröffentlichung und allgemeine Akzeptanz in der globalen Mathematik-Community. OpenAI selbst erklärt, den Preis nicht beanspruchen zu wollen.

Deshalb gilt: Provider-Claim ≠ wissenschaftliche Akzeptanz ≠ institutionelle Anerkennung.

Was ist trotzdem schon jetzt bemerkenswert?

OpenAI berichtet von ungefähr 10.000 koordinierenden Agenten, Werkzeugzugriff, parallelen Suchrichtungen, Austausch von Zwischenergebnissen und anschließender Lean-Formalisation. Falls der Beweis hält, wäre das nicht nur ein mathematisches Resultat, sondern ein starkes Beispiel für AI als produktiven Bestandteil eines Forschungssystems.

Falls Fehler gefunden werden, bleibt die Episode ebenfalls wichtig: Sie zeigt, warum Frontier-Research mit AI Verification, Provenance und unabhängige Kontrolle besonders ernst nehmen muss.

Was wissen wir derzeit?

• Belegt: Paper und Lean-Formalisation sind öffentlich.
• Von OpenAI behauptet: Die Konstruktion erfüllt C und D des offiziellen Millennium-Problems.
• Noch nicht etabliert: allgemeine wissenschaftliche Akzeptanz.
• Neu: Clay bezeichnet das Problem öffentlich als offenbar gelöst; die formale Evaluation und Credit-Zuordnung laufen weiter.
• Offen: Detailkritik, mögliche Korrekturen und Provenance-/Priority-Fragen.

Kurz gesagt