In einem Gespräch des World Science Festival vom 2. Oktoberschilderte der Mathematiker Tristan Buckmaster ein mithilfe von KI erzieltes Ergebnis, das er für korrekt, für andere Mathematiker aber schwer lesbar hält. Sein Bericht macht aus der jüngsten Navier–Stokes-Ankündigung eine konkretere Frage: Wie kann eine Forschungsgemeinschaft ein formales Argument untersuchen, wenn eine verständliche Erklärung zusätzliche Arbeit erfordert?

Buckmaster sprach über seine Arbeit mit Levent Alpöge zu den dreidimensionalen Euler-Gleichungen mit glatter äußerer Kraft. Ihr Ergebnis ist getrennt von OpenAIs Behauptung vom 8. September zu den Navier–Stokes-Gleichungen mit glatter äußerer Kraft. Navier–Stokes berücksichtigt Viskosität; Euler nicht. OpenAI veröffentlichte ein Paper und eine Lean-Formalisierung für sein behauptetes Ergebnis eines Zusammenbruchs in endlicher Zeit. Die für den Millennium-Preis zuständige Institution hat keinen Preis bekannt gegeben.

Die große Veränderung

  • Was sich geändert hat: Buckmaster hat aus eigener Erfahrung berichtet, wie er KI-generierte Argumente und Lean nutzte, um das separate Ergebnis zu Euler mit äußerer Kraft zu begründen, und welche Arbeit noch nötig ist, um solche Beweise Mathematikern zu erklären.
  • Warum das wichtig ist:Eine formale Prüfung kann belegen, dass ein kodiertes Argument aus festgelegten Definitionen und Abhängigkeiten folgt. Mathematiker müssen außerdem verstehen, was der Satz aussagt, wie seine Ideen funktionieren und auf wessen früheren Arbeiten er aufbaut.
  • Worauf zu achten ist:Clays Bewertung der Navier–Stokes-Behauptung von OpenAI, verständliche Darstellungen des Beweises und die öffentliche Auseinandersetzung mit Urheberschaft und Zugang werden zeigen, wie dieses Ergebnis bewertet wird. Buckmasters Zuversicht ist eine Experteneinschätzung, keine Entscheidung über einen Preis.

Auch ein geprüfter Beweis braucht eine Erklärung

Im Gespräch, sagt Buckmaster, habe der erste KI-generierte Beweis für sein Euler-Ergebnis nützliche Ideen mit irrelevanten Berechnungen und schwer lesbarem Text vermischt. Sein Team nutzte zunächst andere Agenten, um einzelne Schritte zu prüfen, und übertrug das Argument anschließend für eine formale Prüfung in Lean. Trotz der schlechten Darstellung sei der entstandene Beweis korrekt gewesen. Diese Schilderung bezieht sich auf seine Euler-Arbeit; sie sollte nicht als seine unabhängige Überprüfung jedes Teils des anderen Navier–Stokes-Papers von OpenAI verstanden werden.

Der Unterschied ist praktisch. Lean prüft eine präzise formalisierte Aussage in einer festgelegten Beweisumgebung. Dadurch wird ein langer Beweis nicht automatisch für Forschende verständlich, die seine Methode weiterverwenden möchten. Buckmaster sagte Brian Greene, andere KI-Systeme hätten Passagen entschlüsseln können, die er kaum lesen konnte; die KI um eine Übertragung in gewöhnliche mathematische Sprache zu bitten, sei Teil der Arbeit geworden. Er sagte auch, dass er die Ideen des Navier–Stokes-Arguments weiterhin verstehen könne, obwohl das veröffentlichte PDF schwer zu lesen sei. Das sind seine Einschätzungen, keine Beweisprüfung von BIG CHANGE; wir haben weder die Lean-Dateien ausgeführt noch eines der beiden Theoreme begutachtet.

Der Bericht von NYU Courant vom 14. September beschreibt Buckmasters und Alpöges Ergebnis als Verlust der Regularität in endlicher Zeit für erzwungene 3D-Euler-Gleichungen mit glatter Kraft und endlicher Anfangsenergie. Demnach wurden drei Arbeiten der Zusammenarbeit in Lean formalisiert; das Ergebnis steht in einer Forschungslinie, die Diego Córdoba und Luis Martínez-Zoroa begonnen haben. Diese Details sind für die Zuordnung von Leistungen wichtig: Ein von einem Modell erzeugter Beweis kann einen bestehenden mathematischen Weg erweitern, ohne die Menschen zu verdrängen, die ihn begründet haben.

Zwei Ergebnisse in einer schnell verlaufenden Entwicklung

OpenAI zufolge erzeugte sein internes Agentensystem zuerst ein Ergebnis zu Euler ohne äußere Kraft und nutzte diesen Ansatz später für seine separate Navier–Stokes-Konstruktion. Die Ankündigung erkennt den Vorrang von Buckmaster und Alpöge bei ihrem Ergebnis zu erzwungenen Euler-Gleichungen an, erklärt aber, der eigene Beweis sei unabhängig entwickelt worden. Buckmaster beschreibt im Gespräch die mathematischen Mechanismen als verwandt und sagt, OpenAI habe eine Idee mit einem kollabierenden Wirbel ergänzt, um die Viskosität zu behandeln. Beide Darstellungen stimmen darin überein, dass es um unterschiedliche Gleichungen und Beweisschritte geht; Fragen zur Chronologie und geistigen Urheberschaft klären sie nicht vollständig.

Die European Mathematical Society begrüßte die Ankündigung, betonte zugleich frühere Arbeiten und forderte Aufmerksamkeit für Urheberschaft, Anerkennung und Zugang zum internen Modell. Die Stellungnahme von Clay vom 11. September erklärte, das Navier–Stokes-Problem sei offenbar gelöst worden; die Bewertung des Erfolgs und die Zuordnung der Verdienste sollten bewusst ohne Eile erfolgen. Buckmaster sagte Greene, er glaube, OpenAI habe eine Lösung. Beides kann zugleich gelten: die positive Einschätzung eines Fachmanns und die fortdauernde Prüfung durch eine Institution.

Der jüngste Rückzug dreier weiterer mathematischer OpenAI-Manuskripte ist ein separates Ereignis. Der gemeldete Vorzeichenfehler ist ein Grund, einzelne Behauptungen getrennt zu prüfen; er belegt nicht, dass derselbe Fehler im Navier–Stokes-Beweis vorkommt. Der Leitfaden von BIG CHANGE zur Repository-Prüfung erklärt, wie sich Manuskriptversionen und Beweisartefakte finden lassen; unsere Einschätzung zur Prüfungskapazität fordert eigene Unterstützung für Erklärung und Prüfung. Der frühere Artikel zu Navier–Stokes dokumentiert den Beginn dieser Entwicklung. Dieses Gespräch ergänzt den Bericht eines praktizierenden Mathematikers darüber, was folgt, wenn ein KI-System ein Argument erzeugt.

Bei einer so folgenreichen Behauptung sind präzise, verständliche Darstellungen, einsehbare formale Artefakte und unabhängige mathematische Reaktionen die nächsten hilfreichen Veröffentlichungen. Jede erfüllt eine andere Aufgabe. Die Geschwindigkeit, mit der ein Beweiskandidat entsteht, macht diese Aufgaben dringlicher; Clays angekündigtes Verfahren lässt zugleich Zeit für eine sorgfältige Prüfung.

Quellen und weiterführende Informationen