KI-Beweis für Jahrhundertproblem: Mathematiker melden Zweifel an

Ein kurzer Satz von OpenAI-Mitgründer Greg Brockman hat eine Debatte neu entfacht: Spitzenmodelle mit viel Rechenzeit würden „zum Motor wissenschaftlicher Entdeckungen“, schrieb er am Wochenende auf X. Als Paradebeispiel gilt OpenAIs im September vorgestellter Beweis zu den Navier-Stokes-Gleichungen, die beschreiben, wie Flüssigkeiten und Gase strömen.

Laut OpenAI arbeiteten rund 10.000 KI-Agenten gleichzeitig an dem Problem, nach etwa 88 Stunden lag das Ergebnis vor: Eine anfangs ruhende Flüssigkeit könne unter einer glatten äußeren Kraft in endlicher Zeit eine Singularität entwickeln, also gewissermaßen „explodieren“. Damit wäre eines der sieben Millennium-Probleme des Clay-Instituts gelöst, auf die je eine Million Dollar ausgesetzt ist. Zur Kontrolle übersetzte eine KI den Beweis in die Prüfsprache Lean, wo ihn der Computer bestätigte.

Genau daran setzt die Kritik an. Mathematiker des King’s College London und der Universität Cambridge argumentieren in einem noch nicht begutachteten Fachaufsatz, die Lean-Fassung stimme nicht mit dem schriftlichen Beweis überein. Falsch sei OpenAIs Ergebnis damit nicht, betont das King’s College – der Text müsse aber unabhängig geprüft werden. Schon Ende Oktober hatte OpenAI mit einer KI-Widerlegung einer Informatik-Vermutung für Aufsehen gesorgt.