AlphaProof Nexus knackt Erdős-Probleme im Schnellverfahren – für ein paar Hundert Franken pro Stück

Google DeepMind hat mit AlphaProof Nexus ein neues System vorgestellt, das mathematische Probleme löst, an denen sich Forscher seit über 50 Jahren die Zähne ausbeissen. Neun von 353 offenen Erdős-Problemen – darunter zwei, die seit 56 Jahren ungelöst sind – fielen autonom. Kostenpunkt pro Problem: einige Hundert US-Dollar an Inferenz-Compute.

Ein Mathematiker im Loop, ein Compiler als Sicherheitsnetz

Was AlphaProof Nexus von früheren Versuchen unterscheidet, ist das Setup. Statt das Sprachmodell die ganze Beweiskette in natürlicher Sprache durchziehen zu lassen – wie es OpenAI mit GPT-5.2 Pro und GPT-5.4 in vergleichbaren Aufgaben gemacht hat – kombiniert DeepMind das Modell Gemini 3.1 Pro mit dem formalen Beweis-Compiler Lean.

Konkret heisst das: Gemini schlägt einen Beweisschritt vor, Lean prüft ihn maschinell, und Fehlermeldungen wandern direkt in den nächsten Versuch zurück. Das Sprachmodell muss damit nicht selbst beurteilen, ob seine Logik stimmt – diese Aufgabe übernimmt der Compiler. Eine bekannte Schwachstelle generativer Modelle wird so umgangen.

Vier Agent-Varianten – und eine überraschende Erkenntnis

Das System besteht aus vier Agent-Stufen mit zunehmender Komplexität. Variante A ist der einfachste Loop aus Gemini plus Lean-Compiler. B fügt Anfragen an AlphaProof dazu, DeepMinds spezialisiertes Reinforcement-Learning-System für Olympiade-Mathematik. C bringt einen evolutionären Mechanismus ins Spiel: Sub-Agenten teilen sich eine gemeinsame Population von Beweis-Skizzen, die mit einem Elo-System bewertet werden. D kombiniert alles.

Für die Erdős-Probleme wurde Variante D eingesetzt. Aber: Eine nachträgliche Analyse zeigt, dass auch der einfachste Agent A alle neun gelösten Probleme schaffte – nur teurer auf den schwierigsten. Die Forscher leiten daraus einen Trend ab: «Eine fortschreitende Verschiebung von spezialisierten trainierten Systemen hin zu einfachen agentischen Loops, je leistungsfähiger LLMs werden.»

Was sonst noch fiel

Neben den neun Erdős-Problemen löste AlphaProof Nexus:

• 44 von 492 offenen Vermutungen aus der Online Encyclopedia of Integer Sequences
• Eine 15 Jahre alte Frage zu Hilbert-Funktionen in der algebraischen Geometrie
• Eine verbesserte Schranke in der konvexen Optimierung

Die Erfolge konzentrieren sich auf Bereiche wie Kombinatorik, konvexe Optimierung und Zahlentheorie – also dort, wo Leans Mathematik-Bibliothek Mathlib ausgereift ist und sich Probleme in handhabbare Teilziele zerlegen lassen. Der grosse Rest blieb ungelöst. Insgesamt liegt die Erfolgsquote bei rund 2,5 Prozent.

Auch ungelöst kann nützlich sein

Mathematiker, die mit dem System gearbeitet haben, berichten von einem Nebeneffekt: Auch gescheiterte Beweisversuche vertieften das Verständnis für ein Problem. Weil die Skizzen formal sind, konnten sich Expertinnen auf die noch offenen Teilziele konzentrieren, statt jedes Argument von Grund auf nachzuprüfen. Die Agenten halfen zudem, fehlerhafte Formalisierungen in der Literatur zu entlarven.

Aktuell wird das System bereits in laufender Forschung zur Quantenoptik und Graphentheorie eingesetzt. Alle Lean-Beweise stehen auf GitHub offen zur Verfügung.

Für dich konkret

Wenn du in einem Forschungsumfeld arbeitest – ETH, EPFL, Universitäten – ist AlphaProof Nexus ein Wink mit dem Zaunpfahl: Formale Beweis-Assistenten sind nicht mehr nur Spielwiesen für Informatiker, sondern werden zu echten Werkzeugen in der Mathematik-Forschung. Lean ist gratis, die Methode ist publiziert, und das DeepMind-Paper liefert eine konkrete Blaupause.

Fields-Medaillen-Träger Tim Gowers nannte einen vergleichbaren OpenAI-Erfolg kürzlich einen «Meilenstein in der KI-Mathematik». Terence Tao bleibt vorsichtig: Die echte Erfolgsquote liege gerade mal bei einem bis zwei Prozent, konzentriert auf einfachere Aufgaben. Genau diese Marke trifft DeepMind mit neun von 353. Aber zwei Probleme, die seit den 1970er-Jahren offen waren, sind jetzt erledigt – und das für den Gegenwert eines mittleren Restaurantbesuchs.

🔗 Quellen: The Decoder, arXiv 2605.22763, GitHub – AlphaProof Nexus Results