Das Repository openai/NavierStokesAndEuler enthält die Lean-4-Zertifikate zu zwei Aussagen. Für jede positive Zähigkeit gebe es im ganzen Raum glatte Anfangsdaten und eine glatte Krafteinwirkung, für die keine global glatte Lösung mit gleichmäßig beschränkter kinetischer Energie existiert; auf dem periodischen Torus gilt Entsprechendes. Beides ordnet OpenAI den Alternativen (C) und (D) der offiziellen Clay-Problembeschreibung zu.
Die zugelassene Krafteinwirkung gehört zur offiziellen Aufgabenstellung. Charles Fefferman verlangt darin den Beweis einer von vier Teilaussagen: In (A) und (B) ist die äußere Kraft null und es geht um die Existenz glatter Lösungen, in (C) und (D) ist eine glatte Kraft mit vorgegebenem Abfall ausdrücklich erlaubt und ein Zusammenbruch gesucht. Das Clay-Institut sprach am 11. September von einem offenbar gelösten Problem; die Prüfung laufe bewusst ohne Eile.
Die Rechenzahlen stammen von OpenAI. Die ersten Agenten starteten am 1. September, nachdem Gerüchte über gelöste Millennium-Probleme aufgekommen waren; am 5. September lag das Ergebnis vor; die Formalisierung in Lean und ihre Prüfung dauerten über GPT-6 Astra weitere 17 Stunden. Über alle Probleme hinweg verschickten die Agenten 4,9 Millionen Nachrichten und 300 Milliarden Ausgabe-Token, auf Navier-Stokes entfielen davon 2,7 Millionen Nachrichten und rund 130 Milliarden Token. MIT Technology Review nennt etwa 10.000 gleichzeitig laufende Agenten und Kosten in Millionenhöhe.
Das rechnende Modell ist nicht Astra. OpenAI schreibt in der eigenen Ankündigung auf X, den Beweis habe eine Gruppe von Agenten mit einem „next-generation model significantly more capable than GPT-6 Astra“ erzeugt; ausgelöst habe den Vorstoß ein sprunghafter Leistungszuwachs bei diesem internen Modell. Veröffentlicht ist es nicht, gemessen hat es niemand von außen.
Die mathematische Grundlage ist älter als der Rechenlauf: Beide beteiligten Gruppen bauten laut Quanta Magazine auf der Kaskadenkonstruktion von Diego Córdoba und Luis Martínez-Zoroa auf. Fefferman nennt die beiden dort die eigentlichen Helden der Geschichte.
Terence Tao warnte am selben Abend auf Mastodon vor den Folgen für die Forschung. Schon das Gerücht, jemand arbeite an einem Problem, könne einen massiven KI-Einsatz auslösen, der es plattmacht, bevor das ursprüngliche Vorhaben ausreifen kann. Weil die Unternehmen weder Fehlschläge noch den Lösungsweg offenlegen, lasse sich nicht mehr erkennen, welche Probleme für KI schwer sind; Forschende könnten aufhören, vielversprechende Richtungen überhaupt noch zu teilen.
Nachtrag vom 9. Oktober 2026: Alexander Bastounis, Fabian Circelli und Anders C. Hansen argumentieren in einem am 6. Oktober auf arXiv eingestellten, noch nicht begutachteten Preprint, der Lean-Beweis entspreche nicht dem Textbeweis. Bei der KI-gestützten Übersetzung nach Lean habe sich der Sinn verschoben; das Zertifikat bestätige daher nicht die veröffentlichte Argumentation.
Aktualisiert am 9. Oktober 2026.