In einem Vorgang, den man nur als das akademische Äquivalent davon beschreiben kann, jemandem ein Klavier auf den Kopf fallen zu lassen und ihn dann zu bitten, die Noten dazu zu begutachten, hat OpenAI diese Woche fast 400 KI-generierte mathematische Ergebnisse veröffentlicht, verteilt auf mehr als 700 Manuskripte. Die Reaktionen aus der Mathematikgemeinde reichten von „umwerfend“ bis „blanker Wahnsinn“ – und das waren noch die höflichen.

Die Sammlung erstreckt sich über Kombinatorik, mehrere Zweige der Geometrie, Zahlentheorie, theoretische Informatik, Algebra, Topologie, Wahrscheinlichkeitstheorie und statistische Mechanik sowie mathematische Physik. Sie ist so umfangreich, dass OpenAI sich verpflichtet fühlte, eine Anleitung zur Navigation durch das weitläufige GitHub-Repository zu veröffentlichen – was ein bisschen so ist, als würde man jemandem eine Karte für ein Gebäude in die Hand drücken, das man gerade in Brand gesteckt hat.

„Allein die gesamte Liste der Abstracts durchzugehen, ist überwältigend“, sagte Álvaro Lozano-Robledo, Professor für Mathematik an der University of Connecticut. Mehrere Mathematiker sagten gegenüber The Verge, dass sie für das Durcharbeiten des rund 40-seitigen Inhaltsverzeichnisses und der Abstracts gut eine Stunde gebraucht hätten. Für die, die zu Hause mitzählen: eine Stunde nur, um die Speisekarte zu lesen.

Unter den Hunderten von Manuskripten finden sich auch Formalisierungen in Lean, einer Programmiersprache und einem Beweisassistenten, mit dem Ergebnisse computergestützt verifiziert werden können. Diese Formalisierungen haben sich als hilfreich erwiesen, um einige frühere mathematische Behauptungen von OpenAI zu bewerten, und geben Forschern die Gewissheit, dass eine Behauptung logisch korrekt ist, selbst wenn sie das dahinterstehende Argument nicht vollständig verstehen – was ein bisschen so ist, als würde man einem Taschenrechner vertrauen, ohne zu wissen, was Division ist.

Doch der Grad der Verifizierung jedes einzelnen Ergebnisses variierte stark. Auf GitHub räumte OpenAI ein, dass die Ergebnisse „sich in unterschiedlichen Stadien der Verifizierung“ befänden und dass „viele, aber nicht alle Manuskripte formalisiert“ worden seien. Zum Zeitpunkt des Schreibens scheint weniger als die Hälfte der Manuskripte in der Sammlung formal beschrieben worden zu sein. OpenAI gab an, dass nur 300 der 719 Manuskripte formalisiert worden seien – etwa 42 Prozent – und dass man „das Repository mit weiteren Formalisierungen aktualisieren werde, sobald wir sie erhalten“. Also bleibt rund 58 Prozent der mathematischen Apokalypse unverifiziert. Schlaf gut.

Mehrere Mathematiker beklagten gegenüber The Verge den Mangel an Formalisierung, besonders angesichts der schieren Anzahl von Ergebnissen. Selbst wenn Lean-Code ein Ergebnis begleitet, ist die Auswertung nicht augenblicklich. Forscher müssen prüfen, ob die Formalisierung tatsächlich beweist, was das Ergebnis behauptet – ein weiterer zeitaufwändiger Prozess. Mehrere, die die Arbeiten durchgingen, sagten, dass selbst dort, wo computervalidierbare Beweise vorlagen, die Qualität uneinheitlich war und die verifizierten Aussagen nicht immer sauber mit den Behauptungen in den begleitenden Manuskripten übereinzustimmen schienen.

Kevin Buzzard, Mathematikprofessor am Imperial College London, sagte, er habe zahlreiche Theoreme in seinem Arbeitsgebiet – der algebraischen Zahlentheorie – identifiziert, von denen nur etwa sechs sofort „herausstachen“. Kaum eines davon schien in Lean formal verifiziert zu sein. „Folglich muss ich entweder möglicherweise nicht korrekten Schrott lesen oder darauf warten, dass andere dasselbe tun, oder darauf warten, dass jemand sie formalisiert, bevor ich mit Sicherheit sagen kann, dass die Ergebnisse überhaupt korrekt sind.“ Buzzards Bedenken wurden von zahlreichen anderen Forschern geteilt, die diese Woche vermutlich anderes zu tun hatten.

Buzzard war keineswegs allein mit seiner Sorge über KI-„Schrott“ – eine Kurzform für minderwertiges, häufig fehlerhaftes KI-generiertes Material, das zunehmend online und in der realen Welt auftaucht, einschließlich wissenschaftlicher Arbeiten. Wie in anderen Bereichen berichteten Mathematiker The Verge, dass sie in den letzten Jahren einen enormen Anstieg solchen Materials festgestellt haben, das mit Tools wie ChatGPT und Claude erstellt wurde. Vieles davon ist verwirrend, schwer zu lesen und zeugt von wenig Verständnis des Themas; besonders schlampig ist es, wenn es darum geht, andere Forscher zu würdigen. OpenAIs frühere mathematische Arbeiten wurden von Experten weithin kritisiert.