OpenAI hat mit „Astra“ ein noch unveröffentlichtes KI-Modell vorgestellt, das zehn seit mindestens einem Jahrzehnt offene Probleme aus Mathematik und theoretischer Informatik gelöst haben soll – jeweils belegt durch einen maschinell überprüfbaren, formalen Beweis.
Beweise, die jeder nachprüfen kann
Für die zehn Ergebnisse veröffentlichte OpenAI ein 249-seitiges Manuskript sowie formale Beweis-Zertifikate im Beweisassistenten Lean 4 – frei auf GitHub unter Apache-2.0-Lizenz. Die Zahl der offenen Beweislücken (der „sorry“-Zähler) liegt bei null: Jeder Schritt ist vollständig verifiziert. Wer will, kann die Beweise selbst gegen das veröffentlichte Repository laufen lassen – die Korrektheit hängt damit nicht mehr am langwierigen Peer-Review.
Was Astra gelöst hat
Zu den Resultaten zählen die explizite Konstruktion einer „nicht-sofischen“ Gruppe – eine seit Michail Gromovs Definition von 1999 offene Frage –, die Widerlegung von Connes’ Rigiditätsvermutung, ein Beweis von Ehrharts Volumenvermutung sowie die Lösung dreier Probleme aus dem Katalog von Paul Erdős, darunter Problem 183 zu mehrfarbigen Ramsey-Zahlen.
Einordnung
Wichtig: Keines der zehn Resultate hat bislang ein reguläres Peer-Review durchlaufen – die formale Verifikation per Lean tritt hier an dessen Stelle. Und das Modell selbst ist noch nicht öffentlich verfügbar. Dennoch gilt der Schritt als bemerkenswerter Beleg dafür, wie KI ernsthaft an vorderster Forschungsfront mitarbeiten könnte.
