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

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.