OpenAI kündigte am 6. Oktober 2026 mathematische Ergebnisse an, die ein internes Frontier-Modell erzeugt hatte, und verlinkte dazu ein Repository auf GitHub. Die Veröffentlichung umfasst laut Unternehmen auch Materialien zu den Beweisen und ihrer Prüfung – darunter Lean-Formalisierungen für viele Beweise.
OpenAI veröffentlichte Ergebnisse aus einem internen Modell
OpenAI bezeichnete den Urheber der Ergebnisse als internes Frontier-Modell. Im Repository veröffentlichte das Unternehmen mathematische Ergebnisse sowie Protokolle für Überarbeitungen und Zitate, zehn Zusammenfassungen der Modellüberlegungen, Schätzungen zum Rechenaufwand und Statistiken zu bearbeiteten Problemen.
Was die Unterlagen zur Prüfung enthalten
Für viele Beweise stellte OpenAI Formalisierungen in Lean bereit. Lean ist eine Programmiersprache und ein Beweisassistent: Ein formal formulierter Beweis lässt sich damit auf seine logischen Schritte prüfen. Die Angabe bezieht sich auf viele Beweise, nicht auf sämtliche veröffentlichten Ergebnisse.
Was die Angabe von drei Stunden bedeutet
OpenAI zufolge entsprach der durchschnittliche Rechenaufwand pro Ergebnis ungefähr drei Stunden Denkzeit mit ChatGPT Pro. ChatGPT Pro dient dabei als Vergleichsmaßstab; die Ergebnisse stammten laut OpenAI aus dem internen Frontier-Modell.
AGMAI fordert Transparenz bei KI-generierter Mathematik
Die Advisory Group on Mathematics and Artificial Intelligence (AGMAI) veröffentlichte am 29. September 2026 Empfehlungen zum Umgang mit KI-generierter Mathematik. Die Gruppe forderte Labore auf, fortgeschrittene mathematische Probleme nicht mit proprietären Modellen zu testen, die für Forschende unzugänglich sind. Für veröffentlichte KI-Ergebnisse empfahl AGMAI außerdem Angaben zum Modell, zu den Prompts, zu zusammengefassten Überlegungen, Zeit- und Rechenaufwand sowie zum Formalisierungsstatus.
OpenAI erklärte, AGMAI konsultiert und deren Empfehlungen bei der Veröffentlichung berücksichtigt zu haben.
