Ein Beweis von 165 Seiten, erzeugt von rund 10.000 parallel arbeitenden KI-Agenten in etwa 88 Stunden, beschäftigt seit dem 8. September die mathematische Fachwelt. OpenAI erklärt, ein noch unveröffentlichtes internes Modell habe eine der sieben Millennium-Fragen der Mathematik beantwortet, nämlich das Verhalten der Navier-Stokes-Gleichungen für strömende Flüssigkeiten. Das Ergebnis wurde zusätzlich maschinell mit dem Beweisprüfer Lean formalisiert. Ob es der Prüfung durch Fachleute standhält, ist bislang offen, und über die Entstehung der Arbeit ist ein Prioritätsstreit ausgebrochen.
Die Navier-Stokes-Gleichungen beschreiben, wie sich zähe Flüssigkeiten und Gase bewegen, vom Wasser in einer Rohrleitung über die Luft um eine Tragfläche bis zum Blut in den Adern. Aufgestellt wurden sie im 19. Jahrhundert von Claude-Louis Navier und George Gabriel Stokes, und Ingenieure rechnen seither täglich mit ihnen, meist mit numerischen Näherungsverfahren am Computer. Mathematisch bleibt jedoch eine Grundfrage offen, die der französische Mathematiker Jean Leray in den 1930er Jahren präzise formulierte. Sie lautet, ob eine anfangs vollkommen glatte dreidimensionale Strömung für alle Zeiten glatt bleibt oder ob sie nach endlicher Zeit in eine Singularität laufen kann, in der die Geschwindigkeit an einem Punkt über alle Grenzen wächst. Ein solcher Zusammenbruch würde bedeuten, dass die Gleichungen an dieser Stelle ihre Gültigkeit verlieren.
Wegen dieser Bedeutung nahm das Clay Mathematics Institute die Frage im Jahr 2000 in die Liste der sieben Millennium-Probleme auf und setzte je eine Million US-Dollar Preisgeld aus. Gelöst ist davon bislang nur die Poincaré-Vermutung, deren Beweis Grigori Perelman im Jahr 2002 vorlegte und für den er das Preisgeld ablehnte. Die offizielle Aufgabenstellung zu Navier-Stokes gliedert sich in vier Teilfragen, die mit den Buchstaben A bis D bezeichnet werden. A und B verlangen den Nachweis, dass Lösungen für immer glatt bleiben, C und D verlangen das Gegenteil, nämlich ein Beispiel für einen Zusammenbruch, wobei sich die Varianten darin unterscheiden, ob eine äußere Kraft auf die Flüssigkeit wirkt und ob der betrachtete Raum unbegrenzt oder periodisch ist.
Genau in diese zweite Kategorie fällt das nun vorgelegte Ergebnis. Nach Darstellung des Unternehmens konstruiert der Beweis eine dreidimensionale Strömung, die zunächst vollständig ruht und auf die anschließend eine glatte äußere Kraft wirkt. Daraufhin zieht sich ein Wirbel spiralförmig zusammen und dreht sich dabei immer schneller, während der Bereich mit der extremen Geschwindigkeit fortlaufend kleiner wird. Dadurch bleibt die gesamte Bewegungsenergie der Flüssigkeit begrenzt, obwohl die Geschwindigkeit im Zentrum zum Zeitpunkt der Singularität unbegrenzt wächst. Nach Angaben in der Veröffentlichung des Unternehmens zum Navier-Stokes-Problem deckt das Resultat die Varianten C und D ab, also den Fall mit äußerer Kraft im dreidimensionalen Raum und auf dem periodischen Torus. Eine kleinere Gruppe von rund 100 Agenten löste zudem die Regularitätsfrage für die kraftfreien Euler-Gleichungen.
Bemerkenswert ist neben dem Inhalt auch das Verfahren. Mehrere Gruppen von Agenten verfolgten parallel unterschiedliche Lösungsansätze, anschließend wurden die brauchbarsten Zwischenergebnisse zusammengeführt und den Gruppen erneut vorgelegt. Rund 10.000 Agenten arbeiteten dabei gleichzeitig, tauschten für dieses eine Problem etwa 2,7 Millionen Nachrichten aus und erzeugten rund 130 Milliarden Wörterbausteine an Text. Über alle bearbeiteten Aufgaben hinweg summierte sich das auf 4,9 Millionen Nachrichten und etwa 300 Milliarden Textbausteine. Der Durchbruch fiel nach etwa 88 Stunden auf den 5. September, danach übernahm das öffentlich verfügbare Modell GPT-6 Astra in weiteren 17 Stunden die Übersetzung in die Sprache des Beweisprüfers Lean. Die Rechenkosten sollen im Millionenbereich gelegen haben.
Lean ist ein sogenannter Beweisassistent, der jeden logischen Schritt einer Argumentation mechanisch nachvollzieht und nur akzeptiert, was sich lückenlos aus den zugrunde gelegten Definitionen ergibt. Läuft die Prüfung durch, gilt der formalisierte Teil als sicher. Die entscheidende Schwachstelle liegt jedoch außerhalb dieser Prüfung, denn ein Beweisassistent kann nicht beurteilen, ob die eingegebenen Definitionen und Aussagen tatsächlich die gestellte Frage abbilden. Fachleute müssen daher nachvollziehen, ob die formalisierten Sätze wirklich der Aufgabenstellung des Clay-Instituts entsprechen und ob der 165 Seiten lange Text die formalisierten Aussagen trägt. Das Institut führt das Problem bislang unverändert als ungelöst, und OpenAI hat erklärt, das Preisgeld nicht beanspruchen zu wollen. Die offiziellen Regeln verlangen ohnehin eine Veröffentlichung in einer anerkannten Fachzeitschrift und eine Wartezeit von zwei Jahren.
Parallel zur fachlichen Prüfung läuft eine Auseinandersetzung über die Entstehung der Arbeit. Nach eigener Darstellung startete OpenAI seinen Versuch am 1. September, nachdem im Umfeld Gerüchte über Fortschritte bei Millennium-Problemen aufgekommen waren, und nahm nach Abschluss der Lean-Prüfung am 6. September Kontakt zu zwei Mathematikern auf, um eine gemeinsame Bekanntgabe anzubieten. Dabei habe sich herausgestellt, dass deren Arbeit ein verwandtes, aber anderes Problem betraf, nämlich die Euler-Gleichungen mit äußerer Kraft. Einer der beiden, Tristan Buckmaster von der New York University, wirft dem Unternehmen dagegen vor, von seiner Arbeit gewusst und deren Ansatz übernommen zu haben, und schildert Druck im Zusammenhang mit der Nennung seines Koautors Levent Alpöge, der beim Unternehmen Anthropic beschäftigt ist. OpenAI bestreitet, auf die fremde Arbeit zugegriffen zu haben, hat die historischen Verweise in der überarbeiteten Fassung des Papiers jedoch erweitert.
Unabhängig vom Ausgang markiert der Vorgang eine Verschiebung. Bisherige Erfolge von Sprachmodellen in der Mathematik betrafen überwiegend Wettbewerbsaufgaben mit bekannter Lösungsstruktur oder das Auffinden bereits publizierter Argumente in der Fachliteratur, was im Frühjahr für Peinlichkeiten sorgte, als angeblich neue Beweise sich als längst veröffentlicht erwiesen. Eine eigenständige Arbeit von 165 Seiten mit maschineller Verifikation liegt fachlich auf einer anderen Ebene. Zugleich zeigt der Aufwand die Grenzen, denn 10.000 gleichzeitig arbeitende Agenten und Rechenkosten in Millionenhöhe stehen keiner Universität zur Verfügung. Sollte der Beweis der Prüfung standhalten, wäre erstmals ein Ergebnis an der Forschungsfront maßgeblich von einer Maschine erzeugt worden. Sollte er scheitern, bliebe die Erkenntnis, dass die Prüfung solcher Arbeiten selbst zur Herausforderung wird, weil kaum jemand hunderte Seiten maschinell erzeugter Mathematik in vertretbarer Zeit vollständig nachvollziehen kann.