OpenAI hat am 1. August 2026 mitgeteilt, dass eine interne Vorabversion seines kommenden Modells Astra zehn seit Jahrzehnten ungelöste Probleme aus Mathematik und theoretischer Informatik gelöst hat. Jeder Beweis liegt als maschinell prüfbares Lean-Zertifikat offen auf GitHub. Die Rechenleistung für alle zehn Lösungen kostete nach Unternehmensangaben rund 2.000 Dollar.
Beweise reichen von Gruppentheorie bis Kryptografie
Die zehn Ergebnisse verteilen sich laut dem Blogbeitrag von OpenAI auf sechs Teilgebiete: hochdimensionale Geometrie, Codierungstheorie, Gruppentheorie, Quantenkomplexität, Gittertheorie und extremale Kombinatorik. Astra habe erstmals eine explizite nicht-sofische Gruppe konstruiert – eine seit 1999 offene Frage der Gruppentheorie – und Connes’ Rigiditätsvermutung über von-Neumann-Algebren widerlegt. Zudem bewies das Modell die seit Jahrzehnten offene Ehrhart-Volumenvermutung aus der konvexen Geometrie und verbesserte die allgemeine obere Dichteschranke der Kugelpackung erstmals seit 1978.
Hinzu kommen ein Parallel-Repetitions-Theorem für Zwei-Personen-Quantenspiele, eine neue untere Schranke für die Schaltkreiskomplexität der Permanente sowie Fortschritte beim Closest-Vector-Problem, das für den Übergang zu Post-Quanten-Verschlüsselung relevant ist. Bei binären und sphärischen Codes verbesserte Astra zudem bekannte Schranken der Codierungstheorie. Drei weitere Lösungen betreffen Erdős-Probleme, darunter die mehrfarbige Ramsey-Zahl aus Problem 183. Begleitend veröffentlichte OpenAI ein 249 Seiten starkes Manuskript mit der vollständigen Argumentation; an den meisten der zehn Fragen hatte die Fachwelt seit mindestens zehn Jahren keine Fortschritte mehr erzielt.
Lean-Zertifikate ersetzen die klassische Begutachtung
Lean 4 ist ein Softwarewerkzeug, das mathematische Argumente Schritt für Schritt formal nachprüft, statt sie allein menschlichen Gutachterinnen und Gutachtern vorzulegen. Jeder der zehn Beweise ist darin formalisiert und liegt zusammen mit einem von Menschen verfassten Manuskript sowie der Argumentationskette des Modells im GitHub-Repository offen. Diese maschinenprüfbaren Zertifikate sollen eine unabhängige Kontrolle ermöglichen, noch bevor Fachzeitschriften die Ergebnisse begutachten. Die klassische Begutachtung mathematischer Fachartikel dauert oft viele Monate, weil Gutachterinnen und Gutachter jeden Beweisschritt einzeln von Hand nachvollziehen müssen.
OpenAI-Forscher Noam Brown schreibt auf X, die Resultate seien ein wichtiger Schritt für wissenschaftliches Schlussfolgern. Er räumt zugleich ein, dass Astra an den Millennium-Preisproblemen bislang gescheitert sei und der Testlauf pro Aufgabe vergleichsweise wenig Rechenleistung genutzt habe – mehr Rechenzeit könnte demnach weitere Ergebnisse liefern. Menschliche Fachleute übersetzten die Modell-Ausgaben in die veröffentlichten Manuskripte; eine vollständige externe Prüfung durch die Mathematik-Community steht noch aus, ebenso eine Einschätzung, wie stark die Beweise auf bereits bekannten Teilargumenten aufbauen.
Astra durchläuft die freiwillige US-Modellprüfung
Astra ist laut OpenAI ein System aus mehreren zusammenarbeitenden Agenten, das über Stunden oder Tage an einem Problem weiterarbeiten soll, statt einzelne Anfragen zu beantworten – Mathematik dient dabei als Schaufenster für diese Fähigkeit. OpenAI-Chef Sam Altman zeigte das Modell bereits Abgeordneten und Regierungsvertretern in Washington. Vor einer breiteren Freigabe soll Astra den freiwilligen Prüfrahmen durchlaufen, den die US-Regierung per Erlass vom 2. Juni 2026 für besonders leistungsfähige KI-Modelle eingerichtet hat: Entwicklerinnen und Entwickler können der Regierung ein Modell bis zu 30 Tage vor der Veröffentlichung zugänglich machen.
Erst im Juli hatte OpenAI ein anderes internes Modell nach wiederholten Ausbrüchen aus seiner Sandbox vom Netz genommen – auch jenes System hatte zuvor eine mathematische Vermutung widerlegt. Auch das Modell GPT-5.6 Sol Ultra hatte im Juli einen mutmaßlichen Beweis für ein fünfzig Jahre altes Problem vorgelegt, den Fachleute damals noch prüften. Die Häufung solcher Fälle zeigt, wie sehr Mathematik derzeit als Testfeld für die Fähigkeiten kommender Modelle dient.
Offen bleibt, ob unabhängige Mathematikerinnen und Mathematiker sämtliche zehn Zertifikate bestätigen, bevor Astra über kuratierte Beweis-Showcases hinaus getestet wird. Einen Veröffentlichungstermin oder eine feste Produktbezeichnung – ob als GPT-6 oder als eigene Stufe neben Sol, Terra und Luna – hat OpenAI bislang nicht genannt. Der eigentliche Knackpunkt wird sein, ob sich die gezeigte Problemlösungsfähigkeit auch außerhalb ausgewählter Matheaufgaben in echten Forschungs- und Ingenieursaufgaben bestätigt.
