Am 8. September 2026 ist zum ersten Mal ein Millennium-Problem der Mathematik von einer Maschine gelöst worden. Ein internes Modell von OpenAI hat für die Navier-Stokes-Gleichungen bewiesen, dass Lösungen in endlicher Zeit zusammenbrechen können. Der Beweis ist in Lean formalisiert, also von einem Programm Schritt für Schritt nachgerechnet. Charles Fefferman, der die Problemstellung im Jahr 2000 aufgeschrieben hat, sagte gegenüber Quanta, er sei begeistert, dass das Problem gelöst sei.
Das ist der bislang größte Einzelbefund für die Leistungsfähigkeit dieser Systeme, und er ist von einer Art, die sich nicht wegdiskutieren lässt: Ein formal geprüfter Beweis ist entweder gültig oder nicht.
Sieben Probleme, in 26 Jahren eines gelöst
Das Clay Mathematics Institute benannte im Jahr 2000 sieben offene Fragen als die wichtigsten der Mathematik und setzte je eine Million Dollar aus. In 26 Jahren fiel genau eine davon: Grigori Perelman bewies die Poincaré-Vermutung, lehnte Preisgeld und Fields-Medaille ab und zog sich aus der Mathematik zurück. Die Navier-Stokes-Frage war seit den 1930er Jahren offen.
Die zweite Lösung entstand in 88 Stunden Rechenzeit, in denen rund 10.000 Agenten gleichzeitig arbeiteten, 2,7 Millionen Nachrichten austauschten und etwa 130 Milliarden Tokens erzeugten. Danach brauchte die Formalisierung in Lean weitere 17 Stunden. Das Paper hat 165 Seiten und nennt als Autor die Firma. Das Preisgeld will sie nicht beanspruchen.
Die Gleichung hinter Tragflächen und Blutfluss
Die Navier-Stokes-Gleichungen beschreiben, wie Flüssigkeiten und Gase strömen:
\(u\) ist die Geschwindigkeit an jedem Ort zu jeder Zeit, \(p\) der Druck, \(\nu\) die Zähigkeit, \(f\) eine von außen wirkende Kraft. Die zweite Gleichung sagt, dass sich die Flüssigkeit nicht zusammendrücken lässt. Praktisch funktioniert das gut: Tragflächen, Wettermodelle und Blutströmungen werden damit gerechnet, und die Vorhersagen stimmen.
Das Millennium-Problem fragt nach etwas anderem. Bleiben die Lösungen für alle Zeiten glatt, oder können sie nach endlicher Zeit zusammenbrechen, so dass die Geschwindigkeit über jede Grenze wächst? Charles Fefferman hat die Frage in vier Varianten aufgeschrieben. Zwei behaupten, dass alles glatt bleibt, zwei behaupten das Gegenteil, jeweils einmal für den ganzen Raum und einmal für den periodischen Fall. Wer eine der vier beweist, hat das Problem gelöst.
Die Strömung, die nach endlicher Zeit explodiert
Die Varianten C und D, also der Zusammenbruch. Es gibt einen glatten Anfangszustand und eine glatte äußere Kraft, unter denen die Lösung nach endlicher Zeit explodiert. Fachleute nennen das einen Blow-up.
Für die Strömungsmechanik in der Praxis ändert sich dadurch nichts. Kein Wasser fließt unendlich schnell; was zusammenbricht, ist das Modell, und zwar unter Bedingungen, die eigens dafür konstruiert wurden. Der Wert liegt darin, dass eine Frage geschlossen ist, die 90 Jahre offen war.
Überrascht hat die Richtung niemanden. Diego Córdoba sagte gegenüber Quanta, vor zehn Jahren habe kaum jemand an solche Singularitäten geglaubt. Inzwischen rechnete die Fachwelt mit ihnen.
Die Methode kommt aus Madrid
Die Strategie stammt von Menschen. Córdoba (Madrid) und Luis Martínez-Zoroa (CUNEF) haben in den vergangenen Jahren ein Verfahren entwickelt, mit dem sich Singularitäten für verwandte Gleichungen konstruieren lassen, unter anderem mit einer geschickt gewählten äußeren Kraft. Fefferman nannte gegenüber Quanta die beiden die eigentlichen Helden der Geschichte, und Tristan Buckmaster brachte für Martínez-Zoroa eine Fields-Medaille ins Gespräch. Ein wichtiger Vorläufer ist die Arbeit von Thomas Hou und Guo Luo, die 2013 numerisch ein Blow-up für die verwandten Euler-Gleichungen fanden.
Das schmälert das Ergebnis nicht, es beschreibt seine Form. Der letzte Schritt war schwer genug, dass ihn seit Jahrzehnten niemand geschafft hat, und er wurde mit Mitteln gemacht, die einer Universität nicht zur Verfügung stehen.
Was Lean prüft und was offen bleibt
Lean ist ein Beweisassistent: Man schreibt den Beweis in einer formalen Sprache auf, und das Programm prüft jeden Schritt. Damit ist die Frage, ob der Beweis Lücken hat, weitgehend erledigt, unabhängig davon, wer oder was ihn aufgeschrieben hat. Liegt ein Ergebnis dagegen nur als Text vor, müssen Fachleute 165 Seiten Argumentation durchsehen, und bei früheren KI-Resultaten war es genau diese Handarbeit, an der die Einschätzung hing.
Eine zweite Frage bleibt, und die beantwortet kein Programm: ob die formalisierte Aussage wirklich die Frage trifft, die gemeint war. Genau diesen Abgleich nennt Quanta als die verbleibende menschliche Aufgabe. Wer in den ersten Meldungen las, die unabhängige Prüfung stehe noch aus, hat es damit zu tun und nicht mit der Korrektheit der Ableitungen. Deshalb steht über dem Ganzen bis auf Weiteres ein „höchstwahrscheinlich“ statt eines Punktes.
Der Streit um die Autorenliste
Buckmaster (NYU) und Levent Alpöge (Anthropic) arbeiteten privat an verwandten Gleichungen und veröffentlichten ihre Ergebnisse am Abend vor der OpenAI-Meldung, ebenfalls mit Lean-Beweisen. Buckmaster wirft OpenAI in einem vierseitigen Statement vor, deren Forschungsweg aufgegriffen zu haben, nachdem die Firma von den Fortschritten erfahren hatte; ihm sei angeboten worden, allein zu publizieren, ohne Alpöge, der bei einem Konkurrenten arbeitet. OpenAI widerspricht: begonnen habe man erst am 1. September aufgrund von Gerüchten, Einblick in die fremde Arbeit habe es nicht gegeben. Ausschließen könne man aber nicht, dass anonymisierte Daten aus der Produktnutzung in die Modelle eingeflossen sind.
88 Stunden Antwort, Jahre Verständnis
Die Millennium-Probleme wurden nicht gestellt, damit am Ende jemand ja oder nein sagt. Sie sollten Methoden erzwingen, an denen sich Verständnis aufbaut. Diesmal liegt die Antwort vor, und das Verständnis, aus dem sie stammt, gehört zwei Mathematikern in Madrid. Diese Arbeitsteilung ist neu, und ob sie sich wiederholen lässt, zeigt sich an den fünf Problemen, die noch offen sind.
Für die Einschätzung dessen, was Sprachmodelle können, ist der Fall unabhängig vom Ausgang des Streits ein Datum. Wie belastbar solche Resultate als Beleg sind, habe ich vor einer Weile an den Erdős-Beweisen durchgespielt: Abschied vom stochastischen Papagei. Dieser hier wiegt schwerer als alles, was dort steht.
Quellen
- OpenAI: On the Navier–Stokes Millennium Prize Problem
- Quanta Magazine: AI Has Solved One of Math's $1 Million Millennium Prize Problems
- Scientific American: OpenAI Claims Blockbuster Math Breakthrough amid Swirl of Controversy
- TechCrunch: OpenAI fought dirty on career-making math problem, says NYU mathematician
- heise online: Navier-Stokes: Möglicher KI-Durchbruch wird von Kontroverse überschattet
- Tristan Buckmaster auf Mastodon: Statement zur gemeinsamen Arbeit mit Levent Alpöge
- DorFuchs: Mathe-News! Navier-Stokes wurde gelöst!
Kommentare
Noch keine Kommentare. Schreib den ersten.
Melde dich an, um zu kommentieren.