Astra löst 10 alte Matheprobleme für rund 2.000 Dollar – und genau das ist die eigentliche Zäsur
OpenAI hat mit einer internen Version seines nächsten großen Modellsystems namens Astra zehn lange offene Probleme aus Mathematik und theoretischer Informatik gelöst. Der Aufwand für die erfolgreichen Läufe lag laut den veröffentlichten Angaben bei rund 2.000 US-Dollar an API-Kosten. Die Beweise wurden in Lean formal verifiziert und auf GitHub veröffentlicht.
Die nackte Zahl ist schon hart genug: Zehn Probleme, teils seit vielen Jahren offen, für einen Betrag, der im Forschungsbetrieb kaum mehr als eine Randnotiz ist. Wenn das belastbar bleibt, verschiebt sich die Schwelle für mathematische Entdeckungen. Nicht, weil Maschinen nun „alles besser“ können. Sondern weil ein neues Werkzeug auftaucht, das aus offenen Fragen plötzlich günstige Suchräume macht.
Besonders wichtig ist der zweite Teil der Meldung: die Lean-Beweise. Genau da trennt sich Show von Substanz. In der KI-Forschung wird viel behauptet, aber formale Verifikation nimmt den Ergebnissen einen großen Teil der Unschärfe. Ein sauberer Lean-Beweis ist keine hübsche Demo und kein schlagfertiger Chat-Auszug. Er ist ein überprüfbares Objekt. Das macht den Unterschied.
Unter den gelösten Aufgaben war laut den veröffentlichten Angaben auch ein Problem, das fast 30 Jahre offen war. Genannt werden Beiträge in Gebieten wie Geometrie, Gruppentheorie und Quantenkomplexität. Außerdem soll Astra die Existenz nicht-sofischer Gruppen gezeigt, Connes’ Starrheitsvermutung gelöst, Ehrharts Volumenvermutung bearbeitet und drei Probleme aus einer Liste von Paul Erdős geklärt haben. Das sind keine Marketing-tauglichen Schulbuchaufgaben. Das sind Treffer in Bereichen, in denen Fachleute lange festhingen.
Der Preis ist dabei fast provokant niedrig. Rund 2.000 Dollar für alle erfolgreichen Runs klingt nach einem Detail. Ist es aber nicht. In der KI wird gern über Trainingskosten geredet, über gewaltige Rechenzentren und Milliardenbudgets. Hier rückt die andere Seite in den Vordergrund: Inferenz als produktiver Forschungshebel. Wenn ein Modell für einen vierstelligen Betrag mathematische Arbeit liefert, die jahrelang niemand schließen konnte, dann bekommt Forschung eine neue Kostenstruktur.
Das hat Folgen weit über die Mathematik hinaus. Erstens für Hochschulen und Institute. Wer Zugang zu solchen Systemen hat, kann mehr Probleme parallel anfahren, mehr Vermutungen testen und formale Beweisketten schneller absichern. Zweitens für die Bewertung wissenschaftlicher Leistung. Wenn eine Maschine einen entscheidenden Suchprozess übernimmt, verschiebt sich die Rolle des Menschen: weg vom kompletten Durchrechnen, hin zur Problemwahl, Kontrolle, Interpretation und Formalisierung. Drittens für die Softwareseite der Wissenschaft. Lean und ähnliche Werkzeuge standen lange am Rand. Solche Ergebnisse ziehen sie ins Zentrum.
Interessant ist auch, wie schnell Nachbauten diskutiert werden. Innerhalb von 24 Stunden meldete Anthropic-Mathematiker Levent Alpoge, fünf der zehn Beweise mit Fable reproduziert zu haben – mit einem generischen Prompt und ohne Internetzugang. Falls sich das bestätigt, wird die Geschichte noch größer. Dann geht es nicht nur um ein starkes internes Modell, sondern um eine neue Klasse von Systemen, die mathematische Forschung robuster automatisieren kann.
Genau hier liegt die harte Einordnung: Der eigentliche Durchbruch ist nicht bloß, dass zehn Probleme gelöst wurden. Der Durchbruch ist die Kombination aus niedrigen Laufkosten, formaler Verifikation und möglicher Reproduzierbarkeit. Erst diese drei Punkte zusammen machen aus einem spektakulären Einzelfall eine technische Verschiebung.
Offen bleibt trotzdem genug. Wie viel Steuerung brauchte das System wirklich? Wie viele Versuche scheiterten vor den erfolgreichen Runs? Wie stark war die menschliche Auswahl bei Problemformulierung, Suchstrategie und Nachbearbeitung? Diese Fragen entscheiden darüber, ob wir auf einen seltenen Ausnahmefall schauen oder auf den frühen Standard einer neuen Forschungsrealität.
Aber selbst mit dieser Vorsicht bleibt der Befund klar: Wenn lange offene Probleme für ein paar tausend Dollar mit formal verifizierten Beweisen geknackt werden, dann ist KI nicht mehr nur Assistenz für Forschung. Dann greift sie in den Erkenntnisprozess selbst ein.
