Zehn offene Probleme, maschinengeprüfte Beweise

OpenAI hat Ergebnisse zu zehn offenen Fragen aus Mathematik und theoretischer Informatik veröffentlicht — Probleme, bei denen das Hauptresultat nach Angaben des Unternehmens seit mindestens einem Jahrzehnt unbewegt war. Gearbeitet hat daran eine interne Fassung von Astra, dem nächsten großen Modell des Hauses. Die Gebiete reichen von Geometrie über Kryptografie bis zur Komplexitätstheorie.

Bemerkenswert ist dabei weniger das Resultat als seine Form. Die Beweise liegen im Repository openai/ten-proofs als Lean-4-Formalisierungen. Ein Beweisassistent nimmt sie an oder eben nicht; wo eine Maschine gegenprüft, hängt das Urteil nicht an der Überzeugungskraft eines Textes. Ergänzt wird das durch ein Paper sowie ein zusätzliches, vom Modell selbst erzeugtes Dokument, das aus unveröffentlichten Reasoning-Spuren rekonstruiert, wie die Beweise zustande kamen.

Die Kosten beziffert OpenAI auf weniger als 2.000 US-Dollar je Problem, gerechnet zu den Token-Preisen von GPT-5.6 Sol. Wenige Tage zuvor hatte Anthropic ein ähnlich gelagertes Ergebnis vorgelegt: kryptografische Schwachstellen, gefunden mit Claude, bei rund 100.000 Dollar an Token.

Was offen bleibt

• Wie viele Probleme ohne Lösung durchliefen, nennt niemand. Ein Preis je Treffer ohne die Zahl der Fehlläufe bleibt eine halbe Angabe.
• Die verwendeten Prompts sind nicht veröffentlicht.
• Astra ist nicht verfügbar. Belegt ist eine Fähigkeit, kein Werkzeug.

Einordnung

Grundlagenforschung liegt weit weg von der App-Entwicklung, der Mechanismus dahinter nicht. Tragfähig wird das Ergebnis erst durch den Beweisassistenten: Das Modell darf beliebig oft danebenliegen, weil eine unabhängige Instanz jede Behauptung prüft. Dasselbe Muster greift überall dort, wo sich Korrektheit maschinell entscheiden lässt — Typprüfung, Tests, Schema-Validierung. Fehlt diese Instanz, wächst mit dem Budget nur die Plausibilität, nicht die Verlässlichkeit.

Der zweite Punkt betrifft die Zahl. 2.000 Dollar je gelöstem Problem klingen nach einer Größenordnung, ohne die erfolglosen Läufe sind sie keine. Wer ein Budget für teure Agentenläufe plant, rechnet nicht mit den geglückten Durchgängen, sondern mit allen.