722 Mathematik-Manuskripte aus einem internen OpenAI-Modell, teils mit Lean-Beweisen

Serguey Asael Shinder07 October 2026, 07:331 Min. Lesezeit

OpenAI hat am 6. Oktober angekündigt, „eine breite Palette neuer mathematischer Ergebnisse“ zu veröffentlichen, die ein unveröffentlichtes internes Modell erzeugt hat – nicht als einzelnes Paper, sondern im GitHub-Repository openai/math.

Was im Repository liegt. Laut README umfasst der Katalog 722 Manuskripte in 372 Familien; eine Familie fasst ein Hauptresultat mit begleitenden Argumenten, Folgerungen oder alternativen Beweisen zusammen und ist nach Fachgebiet eingeordnet. Enthalten sind:

• PDFs und Quellen der Preprints mit Zitierhinweisen je Manuskript;
• eine Lean-Bibliothek und ein Formalisierungskatalog, der angibt, welche Beweise maschinell geprüft sind. „Viele, aber nicht alle“ Manuskripte sind formalisiert;
• gekürzte Zusammenfassungen der Modell-Überlegungen zu 10 Ergebnissen, darunter der Irrationalitätsexponent von π, Kaplanskys Vermutung zur direkten Endlichkeit in Charakteristik zwei und die Isomorphie freier Gruppenfaktoren.

Wie die Ergebnisse entstanden. Dem Modell wurden rund 4.000 Probleme gestellt; die Ausgaben wurden zu Familien zusammengefasst und nach Bedeutung gefiltert. Im Schnitt verbrauchte ein Ergebnis etwa drei Stunden ChatGPT-Pro-Denkzeit. OpenAI nennt zwei Ausnahmen vom festen Verfahren: Arbeiten zu einer nullstellenfreien Region der Riemannschen Zetafunktion und einen Beweis der Hodge-Vermutung für abelsche Varietäten mit komplexer Multiplikation; der Text zur Region Re(s) > 11/12 wurde von Menschen sprachlich überarbeitet.

Was OpenAI selbst einschränkt. Die Sammlung enthält Ergebnisse „in unterschiedlichen Stadien der Verifikation“; manche nicht formalisierte Resultate „könnten Fehler haben“, die rasch korrigiert werden sollen. Korrekturen erscheinen als neue Versionen, frühere bleiben abrufbar. OpenAI hat sich nach eigenen Angaben von der Advisory Group on Mathematics and Artificial Intelligence am Institute for Advanced Study beraten lassen, prüft Alternativen zu GitHub in Händen der Fachgemeinschaft und will Workshops und Konferenzen zu KI-erzeugten Ergebnissen finanzieren. Das Modell selbst ist nicht veröffentlicht; OpenAI arbeite an einer verantwortungsvollen Freigabe.