OpenAI meldet zehn gelöste Mathematikprobleme mit Astra für rund $2,000

Für die Behauptung von OpenAI gibt es eine klare Widerlegungsbedingung. Unabhängige Mathematiker müssen die ursprünglichen Fragestellungen, Annahmen und die Neuheit aller zehn Resultate bestätigen und die Beweise in derselben Lean-4.32.0-Umgebung reproduzieren. Lassen sich die Dateien zwar kompilieren, war eine Aufgabe aber bereits gelöst, ist die formale Aussage enger als das anerkannte offene Problem oder weicht eine entscheidende Annahme von der Fachliteratur ab, müsste die Aussage, Astra habe zehn offene Probleme gelöst, korrigiert werden.

Am August 1, 2026 veröffentlichte OpenAI den Bericht „Ten advances in mathematics and theoretical computer science“. Nach Angaben des Unternehmens löste eine interne Version von Astra zehn Probleme aus hochdimensionaler Geometrie, Codierungstheorie, Gruppentheorie, Quantenkomplexität, Gitterkryptografie und extremaler Kombinatorik. Bei keiner Aufgabe habe es mindestens ein Jahrzehnt lang Fortschritte gegeben; die meisten seien wesentlich länger offen gewesen. The Decoder prüfte die Ankündigung und beschreibt Astra als nächste große Modellfamilie von OpenAI. Ein öffentlicher Veröffentlichungstermin fehlt. Auch die Entscheidung zwischen der Bezeichnung GPT-6 und einer Fortsetzung der GPT-5-Reihe ist dem Bericht zufolge noch nicht gefallen.

Die zehn Ergebnisse sind einzelne Forschungsbehauptungen und kein gemittelter Benchmark. Eine Arbeit konstruiert eine nicht-sofische Gruppe und behandelt damit die Frage, ob jede Gruppe endliche Permutationsapproximationen besitzt. Eine weitere liefert für die Berechnung der Permanente mit arithmetischen Formeln eine Untergrenze von $n^4 / \log n$. Hinzu kommen Resultate zu den Erdős-Problemen 183, 146 und 180. Da OpenAI die Aufgaben aus verschiedenen Disziplinen auswählte, lassen zehn Erfolge keinen Rückschluss auf die Erfolgsquote bei beliebigen Forschungsfragen zu. Das Unternehmen veröffentlichte weder den gesamten Aufgabenpool noch eine vollständige Liste gescheiterter Versuche oder das Auswahlverfahren.

Lean verlagert die Prüfung auf Aussagen und Annahmen

OpenAI stellte für alle zehn Resultate Lean-Formalisierungen sowie eine wissenschaftliche Ausarbeitung und Protokolle des Lösungswegs bereit. Lean kann prüfen, ob jeder formale Schritt aus den kodierten Definitionen, Axiomen und vorherigen Schritten folgt. Dadurch lassen sich ausgelassene algebraische Schritte oder ungültige Verweise in langen Argumenten schwerer übersehen. Die formale Verifikation beantwortet dennoch nur, ob eine formale Aussage aus bestimmten Annahmen folgt. Fachleute müssen klären, ob diese Aussage das ursprüngliche offene Problem korrekt abbildet, das Ergebnis neu ist und die Voraussetzungen anerkannt sind.

Nach Darstellung des Unternehmens halfen menschliche Forscher bei der Ausarbeitung der Texte und der Formalisierung; die mathematischen Argumente stammten von Astra. OpenAI übernimmt die Verantwortung für ihre Richtigkeit. The Decoder zitiert den Mathematiker Thomas Bloom von der University of Manchester, der unter anderem die Konstruktion einer nicht-sofischen Gruppe als bedeutende Nachricht bezeichnet. Der Bericht nennt zugleich eine Einschränkung von OpenAI-Forscher Noam Brown: Das Team scheiterte an weiteren großen Aufgaben, löste keines der Millennium-Probleme und setzte pro Problem nicht besonders viel Testzeit-Rechenleistung ein. Die Veröffentlichung zeigt somit ausgewählte Forschungsergebnisse und keinen Blindtest eines öffentlich verfügbaren Modells.

$2,000 erfassen Token, nicht das gesamte Forschungsprogramm

OpenAI schätzt den Wert der für alle zehn Lösungen verwendeten Token zu Sol-API-Preisen auf ungefähr $2,000. Darin fehlen Aufgabenauswahl, Prüfung durch Forscher, Lean-Formalisierung, fehlgeschlagene Läufe, Modelltraining und Abschreibung der Infrastruktur. Die Summe ist auch kein künftiger Preis für Astra. Sie beschreibt die tokenbasierte Inferenz bekannter erfolgreicher Ausgaben, nicht die Gesamtkosten pro veröffentlichungsfähigem Ergebnis.

In den kommenden drei bis sechs Monaten lassen sich zwei Arten von Belegen prüfen. Externe Forscher können die zehn Lean-Projekte reproduzieren und die Neuheit anhand der jeweiligen Fachliteratur bewerten. OpenAI könnte Zahl und Verteilung der versuchten Aufgaben, Fehlschläge und Rechenleistung je Versuch offenlegen. Die erste Prüfung entscheidet über die Aufnahme der Resultate in den wissenschaftlichen Bestand. Die zweite wäre nötig, um die Leistung von Astra außerhalb der ausgewählten Erfolge für reguläre Forschungsarbeit zu schätzen.

Quellen:

• OpenAI: Ten advances in mathematics and theoretical computer science
• The Decoder: OpenAI announces its next major model Astra by dropping ten previously unsolved math solutions

Weiterführend:

• OpenAI: Ten Advances Lean formalizations