OpenAI: zehn mathematische Resultate in Lean formalisiert – die Rolle des internen Modells

Am 1. August hat OpenAI das Manuskript „Ten Advances in Mathematics and Theoretical Computer Science“ veröffentlicht und die Ergebnisse einem eigenen internen Modell zugeschrieben. Gleichzeitig entstand das GitHub-Repository `openai/ten-proofs`, das die Lean-4-Formalisierungen aller zehn Beweise bereitstellt. Herausragend sind darunter ein verbesserter Exponent für die Kugelpackung – der erste seit 1978 –, die Konstruktion einer nicht-sofischen Gruppe und ein Gegenbeispiel zur Rigiditätsvermutung von Connes. Das Repository ist ein auf mathlib aufbauendes Lean-4.32.0-Projekt unter Apache-2.0-Lizenz: Jede und jeder kann die Beweise mit `lake exe cache get` und `lake build All` neu kompilieren, und ein Ordner ComparatorChallenges erklärt, wie sich die Prüfung unabhängig durchführen lässt.

Die Berichterstattung hat diese Resultate mit „Astra“ in Verbindung gebracht, dem Namen der nächsten Modellfamilie, die OpenAI am selben 1. August angekündigt hat; das Manuskript spricht allerdings nur von „einem internen Modell“, das nicht veröffentlicht wurde. Angaben wie die rund 2.000 Dollar an Token-Kosten oder die 249 Seiten des Dokuments stammen aus Berichten Dritter, denn die offizielle Ankündigungsseite ist derzeit nicht erreichbar. Das Paper dankt menschlichen Mathematikerinnen und Mathematikern für das Gegenlesen und verweist auf eine unabhängige, zeitgleiche Arbeit von Shuoxing Zhou, die teilweise mit Unterstützung von GPT-5.6 Sol entstanden ist.

Laut SiliconANGLE stammen die mathematischen Argumente vom Modell, doch es waren menschliche Forschende, die daraus publikationsfähige Manuskripte gemacht haben: Wie schwer dieser Feinschliff wiegt, ist nicht beziffert. Der Einsatz von Lean 4 verschiebt die Debatte: Ein Zertifikat garantiert die logische Gültigkeit des Beweises, bestätigt aber nicht automatisch, dass die formalisierte Aussage mit dem historischen offenen Problem übereinstimmt – diese Prüfung bleibt Menschensache. Keines der zehn Ergebnisse hat ein förmliches Peer-Review durchlaufen. Der Präzedenzfall wiegt schwer: Im Oktober 2025 erwies sich die Ankündigung, GPT-5 habe zehn Erdős-Probleme „gelöst“, als haltlos, und Thomas Bloom, Kurator von erdosproblems.com, nannte sie eine grobe Fehldarstellung. Zu den zehn heutigen Resultaten spricht derselbe Bloom dagegen von „big news“. Wie der theoretische Physiker Tobias J. Osborne anmerkt, sind die genannten 2.000 Dollar die Kosten der erfolgreichen Token, nicht die Gesamtbilanz aller Versuche – eine Zahl, zu der OpenAI nichts mitgeteilt hat. All das fällt in den Kontext der „Leiden Declaration on Artificial Intelligence and Mathematics“ vom Juni 2026, die laut the-decoder von über 3.000 Mathematikerinnen und Mathematikern sowie von der International Mathematical Union getragen wird und Transparenz, Schutz der Urheberrechte und menschliche Verantwortung für die Ergebnisse fordert.

Die eigentliche Nachricht ist nicht, dass eine Maschine Mathematik betrieben hat – das geschieht seit Monaten –, sondern dass diesmal jedes Ergebnis mit einem neu kompilierbaren Lean-Zertifikat kommt: Um zu urteilen, muss man denen, die es ankündigen, nicht glauben. Solange jedoch das Verhältnis von gescheiterten Versuchen zu Erfolgen Betriebsgeheimnis bleibt, ist die Bewertung der Effizienz dieser Modelle eher eine Glaubens- als eine Statistikfrage.