Über 350 Jahre lag Fermats Behauptung ungelöst herum. 1995 lieferte Andrew Wiles den Beweis, 129 Seiten, und Mathematiker brauchten Monate, um ihn zu prüfen. Seit 2024 arbeitet Kevin Buzzard am Imperial College mit einem Team daran, diesen Beweis in Lean zu formalisieren, also so aufzuschreiben, dass ein Computer jeden Schritt kontrolliert. Geplante Dauer: Jahre. Am 4. September hat Anthropic gemeldet, dass Claude das in elf Tagen erledigt hat.
Was genau passiert ist
Tianyi Peng, Anthropic-Forscher mit einer Gruppe an der Columbia University, wollte testen, wie weit Claude bei der Formalisierung von Fermats letztem Satz kommt. Das Ergebnis: ein vollständiger, von Lean geprüfter Beweis. 13 Millionen Zeilen Lean-Code, 29.500 Zwischentheoreme, rund sechs Milliarden Output-Tokens. Der Beweis ist fünfmal so groß wie Mathlib, die gesamte Community-Bibliothek formalisierter Mathematik, auf der er aufbaut.
Gearbeitet haben Dutzende Claude-Agenten parallel, gesteuert über einen Multi-Agent-Harness auf Basis von Claude Code. Das Modell war ein internes Forschungsmodell, laut Anthropic etwa auf dem Niveau von Fable 5.1. Menschliche Eingriffe beschränkten sich auf gelegentliche Hinweise von Peng, etwa welches Teilgebiet gerade Priorität haben sollte.
Der erste Anlauf ging schief. Die Agenten verloren den Überblick über den Projektstand und hörten auf, sinnvoll zusammenzuarbeiten. Etwa 7 Prozent der Zeilen im finalen Beweis stammen noch aus diesen gescheiterten Versuchen. Funktioniert hat es erst mit Prove2Me, einer offenen Plattform von Pengs Gruppe. Sie hält einen Abhängigkeitsgraphen aller Theorem-Aussagen, aus dem sich die Agenten ihre nächste Aufgabe holen. Aussagen und Beweise liegen in getrennten Dateien, was die Lean-Kompilierung beschleunigt, und jedes Theorem hat eine Beschreibung in natürlicher Sprache, damit Agenten bereits Bewiesenes wiederfinden.
Am 18. August um 02:00 UTC stand die Wurzel des Graphen auf PROVED. Anthropic hat Auszüge aus dem Denkprozess veröffentlicht, in denen Claude das selbst registriert: Historic moment, modulo re-check.
Was Kevin Buzzard dazu sagt
Buzzard ist der Mann, dem hier jemand zuvorgekommen ist, und er hat den Beweis geprüft. Er hat den Code kompiliert, mit dem Comparator geprüft, dass die bewiesene Aussage mit Mathlibs Definition von Fermats letztem Satz übereinstimmt, und in seinem Blog geschrieben: Es stimmt. Der Beweis nutzt nur die drei Standard-Axiome von Lean. Kompilieren dauert fast 20-mal so lange wie Mathlib, und das auf einer Maschine mit 96 Kernen.
Sein Post trägt den Titel „FLT: Anthropic has beaten me to it”, und er ist erstaunlich entspannt dabei. Mathematisch, sagt er, lernt man aus dem Beweis nichts Neues. Die Fachwelt war sich sowieso zu 100 Prozent sicher, dass Wiles recht hat. Was der Beweis zeigt, ist, was Autoformalisierung inzwischen kann. Wenn tausende Seiten Literatur in elf Tagen durchgeprüft werden können, dann wird Forschung bald laufend formalisiert, und Maschinen werden gnadenlos jede Lücke markieren, die bisher mit „bekannt unter Experten” überbrückt wurde. Genau das findet er spannend.
Sein Projekt läuft trotzdem weiter. Er hat der EPSRC zugesagt, Bausteine der modernen Zahlentheorie in Mathlib einzupflegen und ein Dokument zu bauen, mit dem Menschen den Beweis erkunden können. Beides hat Anthropic nicht gemacht. Und Claude hat nicht den modernen Beweis formalisiert, sondern die Darmon-Diamond-Taylor-Darstellung von 1995, plus ein paar Abkürzungen, die nur für Primzahlen ab 37 gelten. Für die kleineren war der Satz schon vorher formalisiert.
Eine Zahl aus seinem Post bleibt hängen: Er hat eine Million Pfund für fünf Jahre bekommen. In den Kommentaren rechnet jemand vor, dass sechs Milliarden Output-Tokens zum API-Preis etwa 300.000 Dollar kosten.
Warum das mehr ist als eine Mathe-Anekdote
Die eigentliche Nachricht steckt für mich im Muster, das dahinter sichtbar wird. Ein Schwarm Agenten, ein gemeinsamer Aufgabengraph, ein Compiler als unbestechlicher Schiedsrichter, und plötzlich wird ein Jahre-Projekt zu einem Zwei-Wochen-Projekt. Anthropic hat das gleich noch einmal kleiner ausprobiert: Drei Forscher mit drei normalen Claude-Max-Abos haben über Prove2Me den Drei-Primzahlen-Satz von Vinogradov in drei Tagen formalisiert.
Der Beweis liegt komplett auf GitHub, mit einer schriftlichen Führung durch die Struktur. Wer Lean kennt, sollte reinschauen. Wer nicht, sollte sich merken: Das Argument „KI-Mathe kann man nicht prüfen” hat gerade ein großes Loch bekommen. Genau dafür ist Formalisierung da.
Quellen: Anthropic: Formalizing Fermat’s Last Theorem, GitHub: anthropics/fermats-last-theorem, Kevin Buzzard: FLT: Anthropic has beaten me to it, SiliconANGLE: Anthropic uses Claude to formalize proof of Fermat’s Last Theorem, Hacker News Diskussion