OpenAI kündigt Astra an – mit zehn gelösten Mathe-Problemen

OpenAI hat am 1. August 2026 einen Bericht mit dem nüchternen Titel «Ten Advances in Mathematics and Theoretical Computer Science» veröffentlicht – und damit zwei Nachrichten auf einmal platziert. Erstens: Eine KI hat zehn offene Probleme der Mathematik und theoretischen Informatik geknackt, an denen laut OpenAI seit mindestens einem Jahrzehnt niemand mehr Fortschritte erzielt hatte. Zweitens: Erzeugt hat die Beweise eine interne Version von Astra – jenem System, das OpenAI hier erstmals offiziell als sein «nächstes grosses Modell» bezeichnet.

Von Kugelpackungen bis zur gestürzten Connes-Vermutung

Die zehn Resultate decken ein beachtliches Spektrum ab – von der Geometrie über Gruppentheorie bis zur Komplexitätstheorie. Die Highlights:

• Kugelpackungen: Astra bestimmte die exakte Stärke einer zentralen Beweismethode für hochdimensionale Kugelpackungen – laut Paper die erste Verbesserung der allgemeinen Packungsschranke seit 1978.
• Connes-Rigiditätsvermutung: widerlegt – ein prominentes offenes Problem aus der Theorie der Operatoralgebren.
• Closest-Vector-Problem: ein neuer Härtebeweis für jenes Gitterproblem, auf dessen Schwierigkeit ein Teil der Post-Quanten-Kryptografie aufbaut – also Verschlüsselung, die auch Quantencomputern standhalten soll.
• Erdős-Probleme: gleich drei Einträge der offiziellen Problemliste des legendären Kombinatorikers Paul Erdős erledigt (Nr. 146, 180 und 183) – darunter zwei widerlegte Vermutungen aus der extremalen Graphentheorie und eine neue Schranke für mehrfarbige Ramsey-Zahlen.

Der Mathematiker Thomas Bloom von der University of Manchester, Betreiber der Plattform erdosproblems.com, nennt die Resultate «big news» – und stuft sie konstruktionstechnisch höher ein als das Gegenbeispiel zur Unit-Distance-Vermutung, über das wir im Mai berichtet haben.

2'000 Dollar für zehn Beweise – und ein Vorbehalt

Bemerkenswert ist die Verifizierbarkeit: Alle zehn Beweise wurden im Beweisassistenten Lean formalisiert – einer Software, die jeden logischen Schritt maschinell prüft – und sind auf GitHub veröffentlicht. OpenAI-Forschende halfen, die Argumente in Papers zu giessen, und übernehmen die Verantwortung für die Korrektheit. Die mathematischen Ideen selbst stammen laut OpenAI aber vom Modell.

Die Tokenkosten für alle zehn Lösungen beziffert OpenAI auf rund 2'000 Dollar zu den API-Preisen von Sol. OpenAI-Forscher Noam Brown dämpft allerdings die Erwartungen: Millennium-Probleme habe man keine gelöst – «sadly, no Millennium Prize Problems (yet)». Und in der Community gibt es einen berechtigten Einwand: OpenAI verrät nicht, wie viele Probleme das Modell insgesamt versuchte und wie viele Anläufe nötig waren. Ohne diese Zahlen bleibt unklar, wie effizient die 2'000 Dollar wirklich waren.

Wem gehört ein Beweis ohne menschlichen Autor?

OpenAI schreibt die Beweise ausdrücklich dem Modell zu: Menschliche Autorschaft für einen vollständig KI-generierten Beweis zu beanspruchen, würde beide Beiträge falsch darstellen, argumentiert das Unternehmen – und verweist auf die Leiden Declaration on AI and Mathematics, die von über 3'000 Mathematikerinnen und Mathematikern unterzeichnet wurde und Transparenz beim KI-Einsatz fordert.

Die Community reagiert gespalten. Fields-Medaillengewinner Timothy Gowers berichtet, GPT 5.6 Pro habe zwei Probleme, an denen er lange gearbeitet hatte, jeweils im ersten Anlauf gelöst – und warnt vor einer «möglichen Zerstörung der mathematischen Kultur», wenn niemand mehr die Expertise aufbaut, solche Resultate zu verstehen. Terence Tao sieht die Gefahr eines «Proof Overload»: Beweise könnten schneller entstehen, als Menschen sie prüfen und einordnen können. Andere, wie der Londoner Professor Abhishek Saha, sehen schlicht ein mächtiges Werkzeug – der Mathematiker werde zum «Dirigenten statt zum ganzen Orchester».

Warum dich das betrifft

Astra ist das Modell, hinter dem OpenAIs Ambitionen für tage- statt minutenlange KI-Arbeit stecken – wir haben über das Long-Horizon-Projekt bereits berichtet. Dass OpenAI den Namen ausgerechnet mit einem Mathe-Paper offiziell macht, ist kein Zufall: Maschinell verifizierte Beweise sind der seltene Fall, in dem sich eine KI-Leistung nicht wegdiskutieren lässt. Zur Einordnung gehört aber auch: Gemäss dem Benchmark-Institut Epoch AI hat KI in den härtesten Problemkategorien («Major Advance», «Breakthrough») noch kein einziges Problem gelöst, und die sechs offenen Millennium-Probleme bleiben unerreicht. Die Werkzeuge werden mächtiger – die wirklich grossen Brocken liegen noch da.