OpenAI veröffentlicht 372 weitere Mathematik-Ergebnisse seines unveröffentlichten Astra-Modells auf GitHub
Zusammenfassung der Neuigkeiten
OpenAI hat eine zweite, deutlich umfangreichere Reihe mathematischer Ergebnisse auf GitHub veröffentlicht: 372 Behauptungen, die alle Astra zugeschrieben werden – einem internen Modell, das das Unternehmen als seine nächste große Veröffentlichung bezeichnet. Laut Berichten vom 6. Oktober 2026 (US-Ostküstenzeit, US-Veröffentlichungsdatum) soll jedes Ergebnis eine offene Frage in der Mathematik oder theoretischen Informatik lösen oder wesentlich voranbringen. Viele davon enthalten maschinell überprüfbare Beweise in der Programmiersprache Lean, doch da das Modell selbst nicht veröffentlicht wurde, können externe Forscher bisher nicht nachvollziehen, wie die Ergebnisse zustande kamen.
Was OpenAI veröffentlicht hat
Die neue Veröffentlichung erfolgt etwa zwei Monate nach OpenAIs erster Ankündigung „Zehn Fortschritte in Mathematik und theoretischer Informatik“ vom 1. August 2026 (US-Ostküstenzeit). Diese erste Serie behandelte zehn langjährige Probleme aus acht Fachgebieten, darunter Gruppentheorie, Operatoralgebren, Kodierungstheorie und extremale Kombinatorik. Sie wurde zusammen mit einem 249-seitigen Manuskript und Lean-4-Zertifikaten in einem öffentlichen GitHub-Repository bereitgestellt, und OpenAI gab an, dass die verwendeten Tokens zu den eigenen API-Tarifen rund 2.000 US-Dollar gekostet hätten.
Die Oktober-Serie ist um mehr als den Faktor 37 größer. Berichte beschreiben 372 Ergebnisse, darunter angeblich eine Lösung der vierdimensionalen Kakeya-Vermutung, Verbesserungen einiger weit verbreiteter Computeralgorithmen sowie teilweise Fortschritte im Zusammenhang mit der Riemannschen Vermutung. OpenAI zufolge stammt fast jedes Ergebnis aus einem einzigen Prompt, der an einen einzelnen KI-Agenten gerichtet wurde. Das Unternehmen gab nur die durchschnittliche Rechenzeit bekannt, nicht jedoch einzelne Prompts oder den Rechenaufwand pro Ergebnis.
Warum Lean-Beweise wichtig sind
Lean ist ein Beweisassistent: ein Programm, das jeden logischen Schritt eines Beweises maschinell überprüft. Wenn ein Ergebnis in Lean formalisiert wird, muss der Leser dem Autor nicht vertrauen. Die Software akzeptiert den Beweis entweder oder lehnt ihn ab. Scientific American berichtet, dass durch die Lean-Validierung die verifizierten Beweise so gut wie sicher korrekt sind.
Dies ist ein anschauliches Lehrbeispiel dafür, wie computergestützte Mathematik funktioniert. Ein Lean-Beweis garantiert, dass eine Aussage aus ihren Annahmen folgt. Er garantiert jedoch nicht, dass die Aussage so formalisiert wurde, wie es ein menschlicher Leser beabsichtigt hat, und er sagt nichts darüber aus, wie der Beweis gefunden wurde.
Was Mathematiker sagen
Die Reaktionen fallen gemischt aus. Andrew Sutherland vom MIT erklärte, dass Behauptungen, Probleme mit einem einzigen Agenten auf Anhieb gelöst zu haben, solange als unbestätigt gelten sollten, bis das Modell veröffentlicht ist und andere die Arbeit reproduzieren können. Daniel Litt von der University of Toronto argumentierte, dass es wenig Grund gebe, sich auf ein Unternehmen zu verlassen, das die Mittel zu deren Erzeugung zurückhält, wenn die Fachgemeinschaft Antworten auf diese Fragen suche. Terence Tao kritisierte das Tempo, mit dem KI-Labore derzeit Ergebnisse produzieren, und nannte es „wahnsinnig“.
Scientific American merkt zudem an, dass OpenAI die Empfehlungen einer unabhängigen Beratergruppe nicht vollständig befolgt habe, dass einige Ergebnisse möglicherweise mehrere Versuche benötigten und dass ein Teil des Materials selbst von OpenAIs eigenen Mathematikern noch nicht verstanden werde. Hunderte Ergebnisse zu prüfen, sei für eine Gemeinschaft menschlicher Experten eine enorme Aufgabe.
Die Zitierdebatte aus der ersten Serie
Am 6. August 2026 (US-Ostküstenzeit) berichtete Scientific American, dass einige Experten bemängelten, Astra habe bei zwei der ersten zehn Ergebnisse frühere Arbeiten nicht angemessen gewürdigt. Stephen Miller von der Yeshiva University sagte, ein Argument zur Kugelpackung aus seiner Arbeit von 2016 sei als originär dargestellt worden. Ein weiteres Ergebnis zur Sofizität in der Gruppentheorie habe Berichten zufolge Ideen aus Veröffentlichungen der Jahre 2016 und 2019 ohne ausreichende Quellenangabe kombiniert. Francesco Fournier-Facio von der University of Cambridge erklärte, die Ankündigung habe entscheidende aktuelle Entwicklungen übersehen, während Andreas Thom von der Technischen Universität Dresden den gruppentheoretischen Beweis als kreativ und zugleich elementar bezeichnete.
OpenAI räumte die Probleme ein. Ein Sprecher sagte, das Unternehmen werde in jener Woche kleine Aktualisierungen vornehmen, entsprechend der üblichen akademischen Praxis.
Worauf man als Nächstes achten sollte
Drei Fragen werden bestimmen, wie diese Ergebnisse aufgenommen werden. Erstens: Wie viele der 372 Behauptungen bestehen eine unabhängige Prüfung und werden in der Fachliteratur anerkannt? Zweitens: Wird OpenAI Astra zugänglich machen, damit die Single-Prompt-Behauptung getestet werden kann? Drittens: Entwickelt das Fachgebiet Normen für das Zitieren früherer Arbeiten und die Anerkennung KI-gestützter Entdeckungen? Für Studierende und Lehrende zeigt dieser Fall sowohl das Potenzial formaler Verifikation als auch die weiterhin bestehende Notwendigkeit menschlicher Peer-Reviews.
Hinweis zu den Quellen
Der Bericht von The Verge zu dieser Veröffentlichung konnte während der Recherche nicht abgerufen werden, daher stammen die obigen Details aus Scientific American und anderen Berichten über OpenAIs Ankündigungen im August und Oktober. Behauptungen zu bestimmten Ergebnissen stammen von OpenAI und wurden nicht alle unabhängig bestätigt.