OpenAI veröffentlichte am 8. September eine vorgeschlagene Lösung des Navier–Stokes Millennium Prize Problems. Das Unternehmen stellt nicht nur einen mathematischen Text bereit, sondern auch eine Formalisierung in Lean. Nach OpenAIs Darstellung erzeugte ein internes Modell den analytischen Beweis, während GPT-6 Astra anschließend bei der formalen Verifikation eingesetzt wurde.
Die Schlagzeile „AI löst ein Millennium-Problem“ ist trotzdem zu grob. Formale Verifikation beantwortet eine andere Frage als wissenschaftliche Anerkennung. Lean kann prüfen, ob ein formalisiertes Argument aus den kodierten Voraussetzungen korrekt folgt. Ob diese Voraussetzungen, Definitionen und die Zuordnung zur offiziellen Problemstellung mathematisch genau das leisten, was behauptet wird, bleibt Gegenstand externer Prüfung.
OpenAI behauptet einen endlichen Singularitätsfall
Das Navier–Stokes-Problem fragt in einer seiner Formen danach, ob aus glatten Anfangsdaten in drei Dimensionen immer glatte Lösungen entstehen oder ob in endlicher Zeit eine Singularität auftreten kann.
OpenAI schreibt, sein System habe eine Konstruktion gefunden, bei der ein zunächst glattes Fluid unter einer glatten äußeren Kraft in endlicher Zeit eine Singularität entwickelt, während die Energie endlich bleibt. Das Unternehmen ordnet das Ergebnis den Aussagen C und D der offiziellen Millennium-Problem-Formulierung zu.
Der physikalisch beschriebene Mechanismus ist ein Wirbel, dessen zentraler Bereich immer kleiner und schneller wird. Mathematisch müssen dabei große Terme aus Beschleunigung, Druck, Impulstransport und Viskosität in einer sehr spezifischen Weise zusammenwirken.
Ob diese Konstruktion die Anforderungen der Clay-Mathematik-Formulierung vollständig erfüllt, ist nicht dadurch entschieden, dass OpenAI sie so einordnet. Dafür braucht es unabhängige mathematische Prüfung.
130 Milliarden Output-Tokens für einen einzelnen Lösungsweg
OpenAI nennt ungewöhnlich konkrete Größenordnungen für die Berechnung.
Für das Navier–Stokes-Projekt seien etwa 2,7 Millionen Agenten-Nachrichten und ungefähr 130 Milliarden Output-Tokens angefallen. Über alle parallel untersuchten Millennium-Probleme hinweg nennt OpenAI 4,9 Millionen Nachrichten und rund 300 Milliarden Output-Tokens.
Der Lösungsweg wurde laut OpenAI nach ungefähr 88 Stunden gefunden. Die Lean-Formalisierung und -Verifikation dauerte weitere 17 Stunden.
Das ist für die Einordnung wichtiger als die übliche Vorstellung eines Modells, das nach einem einzelnen Prompt einen genialen Beweis ausgibt. Die beschriebene Architektur ähnelt eher einer groß angelegten verteilten Suche mit vielen Agenten, Zwischenresultaten, Konsolidierung und anschließender formaler Prüfung.
Fast 100 Agenten arbeiteten bereits am Euler-Vorproblem
OpenAI beschreibt, dass zunächst an mehreren Millennium-Problemen parallel gearbeitet wurde. Ein vorheriger Erfolg beim verwandten Euler-Problem beeinflusste anschließend die Richtung der Navier–Stokes-Suche.
Für die Euler-Regularitätsarbeit seien nahezu 100 Agenten rund 50 Stunden eingesetzt worden. Nachdem dort ein aussichtsreicher Lösungsansatz entstanden war, verschob OpenAI Ressourcen auf Navier–Stokes und gab Agentengruppen unterschiedliche Ansätze.
Codex wurde laut OpenAI verwendet, um Zwischenresultate verschiedener Gruppen zusammenzuführen. Weitere Agenten erhielten diese konsolidierten Erkenntnisse als neuen Kontext.
Damit ist auch dieses Forschungsprojekt ein Beispiel dafür, dass Agentenleistung nicht nur aus Modellqualität besteht. Orchestrierung, Auswahl von Zwischenresultaten und erneute Kontextbildung sind Teil des Systems.
Lean prüft den formalen Beweis, nicht die wissenschaftliche Bedeutung
Lean ist ein interaktiver Theorem Prover. Ein formalisiertes Argument muss jede benötigte Definition und jeden Schluss so präzise angeben, dass der Kernel den Beweis überprüfen kann.
Das reduziert eine wichtige Fehlerklasse. Ein sprachlich überzeugender, aber logisch ungültiger Zwischenschritt kann nicht einfach durch gute Prosa verdeckt werden, wenn die formale Version tatsächlich vollständig geprüft wird.
Es bleibt jedoch eine Übersetzungsschicht. Menschen müssen überprüfen, ob das formalisierte Theorem wirklich dem mathematischen Problem entspricht, das gelöst werden soll. Ebenso muss geprüft werden, ob in Definitionen oder Randbedingungen stillschweigende Annahmen stecken, die die Aussage verändern.
Eine Lean-Verifikation ist deshalb viel stärker als ein unbelegter AI-Beweistext, aber sie ersetzt Peer Review nicht.
Die Entstehungsgeschichte ist ungewöhnlich wichtig
OpenAI erklärt, die Arbeit habe am 1. September begonnen, nachdem das Team von einem Gerücht über Fortschritte von Levent Alpöge und Tristan Buckmaster erfahren habe. Später stellte sich laut OpenAI heraus, dass deren Arbeit ein verwandtes Euler-Problem betraf.
OpenAI gibt an, erst nach Abschluss des eigenen Projekts direkten Kontakt aufgenommen und vorher keinen Zugriff auf deren konkrete Arbeit gehabt zu haben. Das Unternehmen ergänzt außerdem, eine interne Untersuchung habe ergeben, dass Buckmasters frühere Codex-Prompts das verwendete System weder über Training noch auf anderem Weg beeinflusst hätten.
Diese Passage ist kein mathematischer Nebensatz. Bei AI-gestützter Forschung wird Herkunft von Ideen schwieriger zu beurteilen, sobald Modelle mit großen Trainingskorpora, Nutzerinteraktionen und internen Forschungsdaten arbeiten.
OpenAIs Aussage ist hier eine Herstellerangabe über die eigene Untersuchung. Die externe wissenschaftliche Diskussion muss getrennt davon betrachtet werden.
Ein formal verifiziertes Resultat verschiebt die Bewertungsfrage
Bei vielen AI-Forschungsresultaten lautet die erste Frage: Halluziniert das Modell?
Hier ist sie zu eng. Wenn eine formale Beweiskette vollständig durch Lean geprüft wurde, verlagert sich die Prüfung auf andere Ebenen: Entspricht das Theorem der beanspruchten Aussage? Sind Definitionen und Voraussetzungen korrekt? Ist die mathematische Konstruktion neu? Wurde Prior Art vollständig berücksichtigt? Lässt sich der Beweis unabhängig reproduzieren?
Das sind anspruchsvollere Fragen als das bloße Auffinden eines falschen algebraischen Schritts.
Für Softwareentwicklung ist die Struktur trotzdem vertraut. Ein Agent erzeugt ein komplexes Artefakt; ein deterministisches System prüft maschinenlesbare Eigenschaften; Menschen beurteilen anschließend, ob das geprüfte Artefakt überhaupt die richtige Spezifikation erfüllt.
OpenAI hat angekündigt, den Millennium-Preis für das Ergebnis nicht beanspruchen zu wollen. Die praktische Messlatte ist ohnehin eine andere: Wenn unabhängige Mathematiker die Konstruktion bestätigen, wäre nicht nur das Ergebnis bemerkenswert. Ebenso relevant wäre, dass ein Agentensystem mit massiver paralleler Suche und formaler Verifikation ein Forschungsproblem bearbeiten konnte, bei dem die abschließende Qualitätskontrolle nicht auf sprachlichem Vertrauen beruhen muss.