Menschen konnten es in 56 Jahren nicht lösen, Google AI hat in einer Nacht 9 Jahrhundertsprobleme nacheinander gelöst.
Bericht von New Intelligence Yuan
【Einführung】DeepMind hat den neuen mathematischen Agenten AlphaProof Nexus veröffentlicht. Neun offene Erdős-Probleme wurden auf einmal gelöst, wobei das älteste seit 56 Jahren ungelöst war! Alle Beweise wurden durch den Lean-Compiler formell verifiziert und enthalten keine Halluzinationen. Internetnutzer haben erstaunt gerufen: Der Funke des mathematischen Singularität ist entfacht.
Die mathematische Welt ist diesen Monat völlig aus dem Ruder geraten.
Kurz nachdem OpenAI die 80-jährige Erdős-Vermutung widerlegt hatte und die Mathematiker noch nicht von der Überraschung erholt waren,
hat Google DeepMind einen neuen künstlichen mathematischen Agenten namens AlphaProof Nexus veröffentlicht.
Link zur Studie: https://arxiv.org/abs/2605.22763v1
Mit einem Schlag hat er neun seit Jahrzehnten ungelöste offene Erdős-Probleme gelöst. Das älteste davon war ganze 56 Jahre lang ungelöst!
Darüber hinaus betrug die Rechenleistungskosten für jedes Problem nur ein paar hundert US-Dollar.
Das Wichtigste ist, dass dieser Beweis fehlerfrei sein muss.
Jeder Schritt der Deduktion wurde durch den Lean-Compiler formell verifiziert, sodass keine Halluzinationen möglich sind. Wenn der Compiler den Beweis akzeptiert, ist er korrekt.
Es ist erwähnenswert, dass AlphaProof Nexus völlig anders ist als der ursprüngliche AlphaProof, der 2024 einen Silbermedaille beim Internationalen Mathematik-Olympiade gewann.
Der ursprüngliche AlphaProof nutzte nur die verstärkte Lernbaumsuche, während Nexus die große Sprachmaschine, AlphaProof und den Evolutionsalgorithmus kombiniert und sich direkt an die forschungsrelevanten Probleme richtet, die menschliche Mathematiker bisher nicht lösen konnten.
AlphaProof Nexus: Evolutionsalgorithmus + LLM + Lean-Compiler
Die Architektur dieses Systems gliedert sich in vier Ebenen, von einfach bis komplex.
1. Agent A (Grundversion)
Mehrere unabhängige Beweis-Subagenten arbeiten parallel. Jeder Subagent führt mehrfache Dialoge mit Gemini 3.1 Pro durch, modifiziert den Lean-Code mithilfe eines Such- und Ersetzungs-Tools, und der Compiler gibt in Echtzeit Fehlermeldungen zurück. Die Subagenten iterieren und korrigieren auf der Grundlage dieser Rückmeldungen.
2. Agent B
Aufbauend auf Agent A wird AlphaProof als Werkzeug hinzugefügt. Wenn ein Subagent bei einem Teilziel stecken bleibt, kann er AlphaProof aufrufen, um eine durch verstärktes Lernen angetriebene Baumsuche durchzuführen und versuchen, lokale Schwierigkeiten zu überwinden.
3. Agent C
Ein Evolutionsalgorithmus wird eingeführt. Die Subagenten arbeiten nicht mehr unabhängig, sondern teilen sich eine "Populationsdatenbank". Jeder Beweisdraft wird von einem LLM-Bewerter bewertet (mit dem Elo-Bewertungssystem), und die Entwürfe mit hoher Punktzahl werden bevorzugt ausgewählt, mutiert und weiterentwickelt.
4. Agent D (Vollversion)
Der Alleskönner. Der Evolutionsalgorithmus, AlphaProof und Gemini 3.1 Pro arbeiten zusammen. Dies ist die Hauptwaffe von DeepMind, um die Erdős-Probleme in großem Maßstab anzugehen.
Der Kernzyklus des gesamten Arbeitsablaufs ist sehr klar:
Der KI generiert einen Beweisdraft → Der Lean-Compiler verifiziert ihn → Im Falle eines Fehlers gibt er Fehlermeldungen zurück → Die KI korrigiert den Entwurf → Der Compiler verifiziert erneut → Dieser Zyklus wird wiederholt, bis der Beweis vollständig akzeptiert wird oder das Rechenleistungskontingent aufgebraucht ist.
Nehmen wir Erdős #125 als Beispiel. Der Lösungsprozess sieht wie folgt aus:
Zunächst analysiert der Subagent die Problemstruktur mithilfe der Denkkettenmethode, modifiziert dann den Lean-Code durch Suche und Ersetzung und ruft schließlich AlphaProof auf, um die Teilziele zu bearbeiten.
AlphaProof hat drei der sechs Teilziele gelöst. Der Subagent zerlegt dann die verbleibenden "harten Nüsse" in kleinere Lemmata und ruft AlphaProof erneut auf - diesmal werden alle Teilziele gelöst.
Während des gesamten Prozesses war kein menschlicher Mathematiker beteiligt.
Neun Erdős-Probleme: Ein 56-jähriges Rätsel wird endlich gelöst
DeepMind hat die Vollversion Agent D auf 353 formalisierte Erdős-Probleme angewendet. Für jedes Problem wurden maximal 3000 Iterationen erlaubt.
Schließlich wurden neun Probleme gelöst.
Einige der wertvollsten Probleme:
1. Erdős #12 (gestellt 1970)
Existiert eine unendliche Menge A, so dass für beliebige drei verschiedene Elemente a < b, c gilt, dass a nicht b + c teilt, und die Dichte von A unter den ersten N positiven ganzen Zahlen die Größenordnung N^(1/2) erreicht?
Dieses Problem war 56 Jahre lang ungelöst. Mehrere Mathematiker erzielten in der Zwischenzeit teilweise Fortschritte, konnten aber keine vollständige Lösung finden.
Die Lösung der KI kombiniert elegant den chinesischen Restsatz und die Drei-Term-Arithmetische-Progressions-Vermeidungsmengen. Indem eine Reihe sorgfältig entworfener "Blöcke" konstruiert wird, werden sowohl die Dichtebedingungen als auch die Teilbarkeitsbedingungen erfüllt.
2. Erdős #125 (gestellt 1996)
Sei A die Menge aller ganzen Zahlen, die in der Dreierzählung nur die Ziffern 0 und 1 enthalten, und B die Menge aller ganzen Zahlen, die in der Viererzählung nur die Ziffern 0 und 1 enthalten. Ist die untere Dichte der Summenmenge A + B positiv?
Die KI hat bewiesen, dass die Antwort nein ist - die untere Dichte ist null.
Der Kern des Beweises ist eine induktive Verdünnungsargumentation. Durch geschickte Nutzung der diophantischen Approximationseigenschaften von 3^m und 4^k (log4/log3 ist irrational) und durch wiederholtes Finden von zwei Skalen, bei denen die Basen fast übereinstimmen, wird die Dichte schrittweise mit einem Faktor von 0,99 auf null reduziert.
3. Erdős #138 (Variante gestellt 1981)
Strebt die Differenz zwischen den van der Waerden-Zahlen W(k + 1) - W(k) gegen unendlich?
Die KI hat einen äußerst eleganten Beweis geliefert: W(k + 1) ≥ W(k) + k. Der Kerngedanke ist die greedy-Färbungserweiterung - auf der Grundlage einer 2-Färbung ohne einfarbige k-AP werden nacheinander neue Elemente hinzugefügt, und durch ein Widerspruchsargument wird gezeigt, dass die greedy-Strategie nicht scheitern kann.
4. Erdős #846
Dies ist ein Problem über die Kollinearitätseigenschaften von Punktmengen in der Ebene.
Die Konstruktion der KI ist erstaunlich.
Sie bildet jede Kante des vollständigen Graphen K∞ auf einen Punkt in der Ebene ab, codiert die Koordinaten mit einem quadratischen Polynom und verwendet dann den unendlichen Ramsey-Satz, um den Beweis abzuschließen.
Der Lean-Beweiscode für alle neun Probleme ist jetzt auf GitHub öffentlich zugänglich.
Projektlink: https://github.com/google-deepmind/alphaproof-nexus-results
Kann sogar der einfache Agent alle neun Probleme lösen?
Die überraschendste Erkenntnis ist nicht, wie stark die Vollversion Agent D ist, sondern dass
sogar der einfachste Agent A alle neun Probleme lösen kann.
Agent A verfügt weder über einen Evolutionsalgorithmus noch über AlphaProof, sondern nur über mehrere unabhängige LLM-Subagenten und einen Rückkopplungszyklus mit dem Lean-Compiler.
Laut einem Vergleichsanalyse der DeepMind-Team zeigt Agent A auf den meisten Problemen in den Fehlergrenzen fast die gleichen Ergebnisse wie Agent B (die Version mit AlphaProof).
Im Vergleich dazu zeigt Agent D seinen Vorteil hauptsächlich bei den schwierigsten Problemen (z. B. #125 und #138) und kann die Beweise mit einem Kostenvorteil von zwei bis fünf Mal erbringen.
DeepMind führt den Erfolg des Grundagenten auf zwei Faktoren zurück: die starke Leistungssteigerung der LLM selbst und die starke Wirkung der Compiler-Rückmeldung bei der Orientierung der LLM-Deduktion.
Das bedeutet, dass mit zunehmender Stärke der Grundmodelle möglicherweise komplexe Systemengineering-Techniken allmählich von einfachen Agenten-Zyklen ersetzt werden.
Probleme, die heute nur durch die Zusammenarbeit von Evolutionsalgorithmus und AlphaProof effizient gelöst werden können, könnten morgen bereits durch einen einfachen LLM-Compiler-Zyklus gelöst werden.
Im Hinblick auf die Kosten betrug die mittlere Kosten des billigsten Problems (#741(ii)) nur 5 - 7 US-Dollar, und die des teuersten Problems (#152) nicht mehr als 200 - 400 US-Dollar.
Voraussetzung ist jedoch, dass das richtige Modell verwendet wird - wenn AlphaProof allein ausgeführt oder ein kleineres Modell (wie Gemini 3.0 Flash) verwendet wird, kann keines der neun Probleme gelöst werden.
