Eine am 8. Oktober 2026 in Science veröffentlichte Studie berichtet, dass Google DeepMinds AlphaProof Nexus 9 von 353 formalisierten Erdős-Problemen löste und 44 von 492 ausgewählten Vermutungen aus der Online Encyclopedia of Integer Sequences (OEIS) bewies. Zwei der gelösten Erdős-Fragen waren seit 56 Jahren offen. Das System sucht mit Sprachmodellen nach Beweisen, die der Lean-Beweisassistent formal überprüft.
Was AlphaProof Nexus macht
AlphaProof Nexus ist ein Rahmenwerk für die formale Beweissuche: Sprachmodelle erzeugen und überarbeiten Beweisskizzen, während Lean prüft, ob ein vorgeschlagener Beweis zum formalisierten Satz passt. Die Studie erschien in Science; sie beschreibt Ergebnisse aus festgelegten mathematischen Aufgabenmengen.
Was die Ergebnisse messen
Die beiden berichteten Erfolgszahlen beziehen sich auf unterschiedliche Mengen und lassen sich nicht zu einer gemeinsamen Erfolgsquote zusammenfassen.
| Ausgewertete Menge | Bewiesen oder gelöst | Umfang der Auswertung | Geltungsbereich |
| Erdős-Probleme | 9 | 353 | In Formal Conjectures formalisierte Probleme; zwei der gelösten Fragen waren seit 56 Jahren offen. |
| OEIS-Vermutungen | 44 | 492 | Ausgewählte offene Vermutungen aus der Online Encyclopedia of Integer Sequences. |
Die 353 Erdős-Aufgaben waren die in Formal Conjectures formalisierten Fälle, die für den Lauf herangezogen wurden. Sie stehen für einen Teil der umfassenderen Sammlung von Erdős-Problemen. Die OEIS-Zahl stammt aus einer eigenen Auswahl offener Vermutungen und hat daher einen anderen Nenner.
Wie die Beweissuche funktioniert
Der beschriebene Ablauf setzt bei einem Lean-Theorem und einer Beweisskizze an. Zusätzlicher natürlicher Sprachkontext und in Lean kodiertes Fachwissen können ebenfalls einfließen. Sprachmodell-Agenten überarbeiten den Beweisversuch; Lean gibt mit seinen Compiler-Rückmeldungen Auskunft darüber, ob der formale Beweis kompiliert.
Die erweiterte Konfiguration ergänzt diese Schleife um evolutionäre Suche: Sie verwaltet und bewertet mehrere Beweisskizzen und kann AlphaProof für Teilziele aufrufen. Das ist etwas anderes, als eine beliebige mathematische Frage in Alltagssprache entgegenzunehmen und sie vollständig selbst zu formalisieren.
Was die Resultate aussagen
Lean prüft einen formalisierten Satz samt Beweis. Ob diese Formalisierung die ursprünglich gemeinte mathematische Frage korrekt wiedergibt, ist eine separate Aufgabe. Für die Erdős-Fälle berichtet die Studie von einer zusätzlichen fachlichen Prüfung der Formalisierungen.
Die meisten ausgewerteten Erdős-Probleme blieben ungelöst. Die beschriebenen Erfolge konzentrierten sich auf Gebiete wie Kombinatorik, konvexe Optimierung und Zahlentheorie, in denen ausgereifte mathematische Lean-Bibliotheken und zerlegbare Teilaufgaben die Arbeit unterstützen.
