Was im Bericht steht: Der Abstract listet zehn Ergebnisse. (1) Hochdimensionale Kugelpackung – die asymptotische Stärke des Cohn-Elkies-Linearprogramms wird exakt bestimmt; daraus folgt ein verbesserter allgemeiner Packungs-Exponent von 0,6044… gegenüber dem klassischen Kabatianskii-Levenshtein-Wert 0,59905576…, was der Bericht als „the first improvement since 1978 to the general sphere-packing exponent“ bezeichnet. (2) Binäre und sphärische Codes – klassische obere Schranken werden „by exponential factors for all parameters“ verbessert. (3) Nicht-sofische Gruppen – eine explizite nicht-sofische Gruppe wird konstruiert und damit die Frage entschieden, ob jede abzählbare Gruppe endliche Permutations-Approximationen zulässt; das Argument nutzt Property-(T)-Expander und die binäre Leavitt-Algebra. (4) Connes’ Rigiditätsvermutung – unendlich viele paarweise nicht isomorphe Property-(T)-Gruppen mit derselben Gruppen-von-Neumann-Algebra widerlegen die Vermutung. (5) Arithmetische Schaltkreis-Komplexität für die Permanente. (6) Exponentielle Parallelwiederholung für jedes endliche verschränkte Zwei-Spieler-Spiel. (7) Härte des Closest-Vector-Problems über eine direkte Reduktion von 3SAT. (8) Ehrharts Volumenvermutung mit der scharfen Schranke (n+1)^n/n!. (9) Multicolor-Ramsey-Zahlen: eine superexponentielle untere Schranke zeigt R_k(3) = k^Θ(k). (10) Zwei Gegenbeispiele in der extremalen Graphentheorie, die die Kompaktheitsvermutung von Erdős und Simonovits sowie eine Degeneriertheits-Vermutung von Erdős widerlegen.
Die Zertifikate: Zu allen zehn Ergebnissen liegt im öffentlichen Repository openai/ten-proofs (Apache-2.0) je eine Lean-4-Formalisierung. Gebaut wird gegen Lean 4.32.0 mit mathlib und Lake; die README beschreibt den Weg über elan, `lake exe cache get` und `lake build All` und verweist für die unabhängige Nachprüfung auf ein eigenes Verzeichnis (ComparatorChallenges). Was das leistet: Ein Lean-Build, der durchläuft, belegt, dass der formalisierte Satz aus den Axiomen von mathlib folgt – ohne dass ein Mensch die Beweiskette liest. Was es nicht leistet: Ob die formalisierte Aussage die klassische Vermutung trifft, entscheidet weiterhin die Lektüre der Definition. Diese Restarbeit ist klein gegenüber dem Gutachten eines mehrhundertseitigen Manuskripts, aber sie ist nicht null.
Zum Modell: Der Bericht spricht durchgehend nur von „an internal OpenAI model“ und nennt keinen Namen. Die Zuschreibung an „Astra“ stammt aus OpenAIs eigener Kommunikation um den Bericht herum – Sébastien Bubeck schreibt auf X, nicht-sofische Gruppen existierten und dies sei „one of many new beautiful results proved by Astra, our next major model“, man veröffentliche „10 such Astra proofs, complete with lean certificates and CoT walkthroughs for each of them“. Der Nachrichtendienst The Information hatte Astra zuvor unter Berufung auf drei mit den Plänen vertraute Personen als neue Modellfamilie beschrieben, die mehrere Agenten über Stunden oder Tage an einem Problem zusammenarbeiten lässt; Sam Altman habe sie in Washington Politikern und Aufsichtsbehörden vorgeführt. Offen ist demnach selbst der Name: OpenAI habe noch nicht entschieden, ob die Familie als GPT-6, als GPT-5.7 oder als eigene Klasse neben Sol, Terra und Luna erscheint. Ob es sich um dasselbe Langhorizont-Modell handelt, dem OpenAI im Mai die Widerlegung der Erdős-Vermutung über Einheitsabstände zuschrieb und dessen internen Zugang das Unternehmen im Juli nach zwei Sandbox-Ausbrüchen pausierte, sagt OpenAI nicht – wir stellen die Verbindung deshalb nicht her.
Kosten und Urheberschaft: Die Token, die zum Auffinden aller zehn Lösungen nötig waren, hätten zu den API-Preisen von Sol rund 2.000 US-Dollar gekostet – eine Angabe des Anbieters, die sich von außen nicht nachrechnen lässt. Zur Arbeitsteilung stellt OpenAI klar, dass das System die mathematischen Argumente erzeugt habe, während das Unternehmen bei der Erstellung der Manuskripte und der Formalisierung in Lean geholfen habe; ausdrücklich verweist es dabei auf die Leiden Declaration, deren erste Empfehlung an einzelne Mathematiker lautet, eingesetzte Werkzeuge offenzulegen.
Was die Beleglage hergibt und was nicht: Das PDF und das Lean-Repository haben wir selbst geöffnet, die zehn Ergebnisse und die Formalisierungen sind belegt. Die Ankündigungsseite auf openai.com war für unseren Abruf gesperrt (HTTP 403); die dort stehenden Angaben zu Kosten, Urheberschaft und Modellnamen sind über zwei unabhängige Wiedergaben belegt und bleiben anbieter-selbstberichtet. Eine unabhängige mathematische Begutachtung liegt zu keinem der zehn Ergebnisse vor – die Reaktionen aus dem Fach sind bisher erste Einschätzungen: Thomas Bloom (University of Manchester, Betreiber von erdosproblems.com) stuft die Konstruktionen laut The Decoder höher ein als das Erdős-Gegenbeispiel vom Mai; Noam Brown von OpenAI schränkt selbst ein, es seien „bisher“ keine Millennium-Probleme darunter.