OpenAI hat 722 Manuskripte mit KI-generierten Lösungen zu 377 bislang ungelösten mathematischen Problemen veröffentlicht, darunter einen Beweis der Unique Games Conjecture und einen formellen Beweis zum Navier-Stokes-Gleichungssystem in der Programmiersprache Lean. Die Meldung, zuerst über faz.net berichtet, löste zunächst Begeisterung in Teilen der KI- und Mathematikgemeinschaft aus, da sie einen potenziellen Durchbruch bei der automatisierten Theoremenbewältigung nahelegt. Doch schon kurze Zeit später meldeten Forschende der University of Cambridge Unstimmigkeiten in der Formalisierung des Navier-Stokes-Beweises. Laut ihrer Analyse könnte ein Fehler bei der Übersetzung des mathematischen Arguments in die formale Sprache Lean vorliegen, wodurch der Beweis zwar syntaktisch korrekt erscheint, aber semantisch nicht unbedingt das intendierte Theorem abdeckt.
Dieser Vorfall unterstreicht ein zentrales Problem beim Einsatz von KI in der Mathematik: Die Erzeugung eines formell verifizierbaren Beweises garantiert nicht automatisch dessen mathematische Korrektheit, wenn die Formalisierung selbst fehlerhaft ist. Zwar prüft Lean die logische Konsistenz des Codes, doch es kann nicht erkennen, ob die zugrundeliegenden Definitionen und Annahmen dem ursprünglichen mathematischen Problem entsprechen. In diesem Fall könnte beispielsweise eine zu starke Vereinfachung der Anfangsbedingungen oder eine falsche Modellierung des Druckterms die Gültigkeit des Beweises für die echte Navier-Stokes-Gleichung unterminieren, selbst wenn der Lean-Code keine inneren Widersprüche aufweist. Solche subtilen Abweichungen sind besonders gefährlich, weil sie von automatisierten Prüftools nicht erfasst werden und erst durch fachkundige manuelle Nachkontrolle sichtbar werden.
Die Reaktion der Fachwelt war entsprechend differenziert. Während einige Expertinnen und Experten die Leistung als technischen Fortschritt hervorhoben – schließlich ist die Erzeugung von 722 formellen Manuskripten eine beachtliche Ingenieursleistung – betonten andere die Notwendigkeit stärkerer unabhängiger Überprüfungsmechanismen. Besonders hervorgehoben wurde die Rolle von Proof-Assistants wie Lean nicht als Ersatz für mathematisches Urteil, sondern als Werkzeug, dessen Output stets von Spezialistinnen und Spezialisten validiert werden muss. Einige Mathematiker forderten öffentlich standardisierte Protokolle für die Überprüfung KI-generierter Beweise, ähnlich wie es sie in der Softwareentwicklung für Sicherheit kritischer Systeme gibt. Andere wiesen darauf hin, dass dieser Fall kein Einzelfall sei: Ähnliche Probleme traten bereits bei der Formalisierung des Feit-Thompson-Satzes in Coq auf, wo zunächst übersehene Annahmen erst nach Monaten entdeckt wurden.
Langfristig könnte dieser Vorfall Einfluss darauf haben, wie KI-Systeme in der mathematischen Forschung eingesetzt und bewertet werden. Anstatt reine Beweisproduktion zu belohnen, könnten zukünftige Benchmarks stärker auf die Nachvollziehbarkeit und fachliche Präzision der Formalisierung achten. Auch die Zusammenarbeit zwischen KI-Entwicklern und Mathematikern könnte intensiver werden, um sicherzustellen, dass die Übersetzung von informellen mathematischen Ideen in formale Sprachen nicht nur maschinell korrekt, sondern auch inhaltlich treu bleibt. Ohne solche safeguards besteht die Gefahr, dass KI nicht echte mathematische Fortschritte produziert, sondern lediglich eine Illusion von Rigorosität erzeugt – eine Entwicklung, die sowohl das Vertrauen in KI-Tools als auch die Integrität der mathematischen Forschung unterminieren könnte.
