Laut der Änderungsliste im Repository openai/math liegt der Fehler in der Arbeit „Algebraicity of Weil classes on split abelian eightfolds“. Er macht dort ein Kürzungsargument ungültig und trifft zwei abhängige Arbeiten zu K3-Flächen, darunter eine zur rationalen Hodge-Vermutung. Die zurückgezogenen Texte bleiben mit Hinweis archiviert. 14 Manuskripte erhielten Beweisreparaturen, korrigierte Aussagen oder klarere Voraussetzungen, 13 weitere nur aktualisierte Verweise. Wer den Fehler gefunden hat, sagt OpenAI nicht.
Mit sechs neuen Formalisierungen liegen nach OpenAIs Zählung 300 der 719 Hauptergebnisse als maschinenprüfbare Beweise im Beweisassistenten Lean vor. Die Gedankenketten des Modells sind für zehn Manuskripte beigelegt. Laut TechCrunch hatte die Advisory Group on Mathematics and AI, die OpenAI berät, empfohlen, schwer nachvollziehbare Beweise zu formalisieren und offenzulegen, wie die Modelle zu ihren Ergebnissen kamen.
Dass ein Lean-Beweis allein nicht genügt, argumentieren Alexander Bastounis, Fabian Circelli und Anders C. Hansen in einem am 6. Oktober auf arXiv eingestellten Preprint. Übersetze eine KI einen Textbeweis nach Lean, könne sich der Sinn verschieben, und die Maschine prüfe dann eine andere Aussage. Als Beispiel nennen sie OpenAIs Navier-Stokes-Beweis vom September: Der Lean-Beweis entspreche nicht dem Textbeweis. Begutachtet ist das Preprint noch nicht.
Die Harvard-Mathematikerin Melanie Wood beschrieb gegenüber TechCrunch die Lage nach solchen Veröffentlichungen: Zum Zeitpunkt der Freigabe verstehe kein Mensch die Ergebnisse, die eigentliche Arbeit beginne erst danach.