Anthropic: Claude-Agenten erstellen ersten computergeprüften Beweis von Fermats letztem Satz

Claude-Agenten formalisieren Fermats letzten Satz in Lean

Anthropic hat am 4. September bekanntgegeben, dass ein Team von Claude-Agenten über elf Tage den ersten vollständigen computergeprüften Beweis von Fermats letztem Satz in Lean erstellt hat. Die Agenten arbeiteten weitgehend autonom und wurden über die Plattform Prove2Me koordiniert. Dabei nutzten sie eine geteilte Aufgabenliste, die als gerichteter azyklischer Graph das gemeinsame Gedächtnis des Teams bildete: Jeder Agent übernahm Teilaufgaben, formalisierte Zwischentheoreme und Definitionen und gab seine Ergebnisse zur Prüfung durch den Lean-Kernel frei. So konnten Dutzende Agenten parallel arbeiten, ohne sich gegenseitig zu überschreiben. Es handelt sich um eine Formalisierung des bestehenden Wiles-Beweises von 1995, keine neue mathematische Entdeckung. Die Formalisierung folgt der Darmon-Diamond-Taylor-Darstellung, weil diese den Beweis über Frey-Kurven und den Satz von Ribet in klar getrennte Module zerlegt, die sich für die schrittweise maschinelle Prüfung eignen. Zuvor existierten nur Teilformalisierungen oder gescheiterte Versuche; die Besonderheit liegt in der schieren Größe des erzeugten Codes und der Koordination dutzender Agenten.

13 Millionen Zeilen Code und dutzende koordinierte Agenten

Der erzeugte Lean-4-Beweis umfasst etwa 13 Millionen Zeilen und rund 29.500 Zwischentheoreme; eine Quelle nennt 29.511 Theoreme und 1.450 Definitionen. Die Code-Größe ist ein Indikator für den Aufwand, weil Lean jeden noch so trivialen Schritt explizit verlangt – ein menschlicher Beweis überspringt viele Zwischenschritte, die hier alle ausformuliert werden müssen. Damit ist der Code mehr als fünfmal so groß wie die Community-Bibliothek Mathlib. Dutzende Claude-Agenten koordinierten sich über Prove2Me und verbrauchten etwa sechs Milliarden Output-Token; diese Token-Menge misst die vom Modell erzeugten Code- und Texteinheiten und spiegelt die schiere Menge an generierten Beweisschritten wider. Die Verifikation erfolgte durch den Lean-Kernel sowie einen unabhängigen Rust-Kernel namens nanoda, der als zweite Instanz Fehler im Lean-Kernel selbst ausschließen soll. Verwendet wurden nur die drei Standard-Axiome von Lean, auf denen auch Mathlib aufbaut, ohne zusätzliche Annahmen. Die Formalisierung folgt der Darmon-Diamond-Taylor-Darstellung über Frey-Kurven und den Satz von Ribet. Der Beweis ist damit der erste vollständige, maschinell geprüfte Beweis von Fermats letztem Satz; die Arbeit zeigt, dass Autoformalisierung in der Lage ist, KI-generierte Mathematik zu prüfen und den bestehenden mathematischen Korpus zu auditieren.