Anthropic hat am 4. September 2026 eine vollständige, von Lean geprüfte Formalisierung von Fermats letztem Satz veröffentlicht. Claude arbeitete dafür laut Anthropic über elf Tage weitgehend autonom. Das Ergebnis umfasst rund 13 Millionen Zeilen Lean-Code und 30.300 bewiesene Zwischentheoreme, von denen etwa 29.500 in der finalen Beweiskette verwendet werden.
Die Schlagzeile klingt zunächst nach einem neuen mathematischen Beweis. Das ist nicht passiert. Fermats letzter Satz wurde 1995 von Andrew Wiles bewiesen. Neu ist die vollständige Formalisierung: Die Argumentation wurde so in Lean übersetzt, dass ein Proof Assistant jeden logischen Schritt maschinell prüfen kann.
Für Softwareentwicklung und Agentensysteme ist vor allem interessant, warum die ersten Versuche scheiterten und was Anthropic danach geändert hat.
Mehrere Agenten reichten zunächst nicht
Anthropic beschreibt, dass frühe Versuche trotz erster Fortschritte festliefen. Die Agenten verloren den Überblick über den Zustand des Gesamtprojekts und koordinierten sich zunehmend schlechter. Teile dieser gescheiterten Arbeit blieben im späteren Ergebnis erhalten und machen laut Anthropic ungefähr sieben Prozent der Nicht-Boilerplate-Zeilen aus.
Das Problem war damit weniger die Fähigkeit eines einzelnen Modells, Lean-Code zu schreiben. Es fehlte eine Struktur, in der viele parallele Agenten wissen, welche Teilaufgabe bereits gelöst ist, welche Abhängigkeiten bestehen und welche Ergebnisse wiederverwendet werden können.
Der erfolgreiche Lauf verwendete deshalb Prove2Me, eine offene Plattform für kollaborative mathematische Formalisierung. Zusammen mit einem auf Claude Code basierenden Multi-Agent-Harness organisierte Prove2Me die Arbeit über einen gerichteten azyklischen Graphen von Theoremen.
Ein DAG wurde zum gemeinsamen Projektzustand
Jeder Knoten in diesem Graphen beschreibt ein Theorem, das für spätere Teile der Beweiskette benötigt wird. Agenten konnten anhand dieses Zustands entscheiden, welches offene Teilproblem als Nächstes bearbeitet werden sollte. Bereits bewiesene Ergebnisse standen anderen Agenten zur Verfügung.
Anthropic nennt drei Funktionen von Prove2Me, die für den Lauf relevant waren. Der DAG reduzierte den Verlust des Projektzustands bei langen Läufen. Theorem-Statements und Beweise wurden in getrennten Dateien gehalten, was die Lean-Kompilierung beschleunigte und Ressourcen sparte. Zu jedem Theorem gab es zusätzlich eine natürlichsprachliche Beschreibung, über die Agenten bestehende Ergebnisse leichter suchen und wiederverwenden konnten.
Das ähnelt Problemen, die auch bei Coding-Agenten auftreten. Ein einzelner Agent kann über Stunden Dateien ändern. Sobald mehrere Agenten parallel arbeiten, reicht ein gemeinsamer Prompt oder Chatverlauf aber kaum als Projektzustand. Es braucht explizite Abhängigkeiten, Artefakte, Statusinformationen und Regeln dafür, wann eine Teilaufgabe als abgeschlossen gilt.
Sechs Milliarden Output-Tokens sind Teil des Ergebnisses
Anthropic gibt an, dass der erfolgreiche Lauf ungefähr sechs Milliarden Output-Tokens eines internen Forschungsmodells verbrauchte, dessen Leistungsniveau ungefähr Claude Fable 5.1 entspreche. Das ist eine Herstellerangabe und kein unabhängiger Kostenbenchmark. Anthropic veröffentlicht für diesen Versuch keine vollständige Kostenrechnung.
Die Größenordnung ist trotzdem relevant. Der Versuch war kein einzelner langer Chat, sondern ein verteiltes System aus Dutzenden Agenten, Proof-Assistant, gemeinsamer Zustandsverwaltung und sehr viel Modellinferenz.
Das fertige Artefakt ist ebenfalls ungewöhnlich groß. Mit rund 13 Millionen Zeilen Lean ist es laut Anthropic mehr als fünfmal so groß wie Mathlib, die zentrale Lean-Bibliothek, auf der die Formalisierung aufbaut. Anthropic weist selbst darauf hin, dass das Ergebnis wahrscheinlich deutlich länger ist als nötig.
Für einen Agentenbenchmark wäre daher nicht nur interessant, ob die Aufgabe am Ende gelöst wurde. Man müsste auch betrachten, wie viel redundante Arbeit entstanden ist, wie häufig Teilpfade verworfen wurden und wie stark der Harness die Suche einschränken musste.
Die Verifikation ist hier stärker als bei normalem Agent-Code
Lean prüft die formale Beweiskette algorithmisch. Anthropic gibt an, dass die fertige Formalisierung nur die drei Standardaxiome von Lean verwendet und dass ein Comparator bestätigt hat, dass die formulierte Aussage mit der Fermat-Definition in Mathlib übereinstimmt. Der Mathematiker Kevin Buzzard, der seit 2024 ein Community-Projekt zur Formalisierung von Fermats letztem Satz leitet, begutachtete das Ergebnis und bezeichnete es gegenüber Anthropic als außergewöhnliche Autoformalisation.
Damit hat dieser Versuch eine Eigenschaft, die normalen Coding-Agenten oft fehlt: Es gibt einen sehr starken automatischen Verifier. Ein Pull Request kann Tests bestehen und trotzdem fachlich falsch sein. Ein formaler Beweis ist wesentlich härter definiert; Lean akzeptiert die Beweiskette oder lehnt sie ab.
Das erklärt einen Teil des Erfolgs. Der Agent produziert nicht nur Text, sondern arbeitet in einer Umgebung, die ihm ständig maschinell überprüfbares Feedback gibt.
Für Coding-Agenten ist der Harness die interessantere Nachricht
Aus dem Projekt würde ich nicht ableiten, dass ein Modell nun beliebige jahrelange Wissensarbeit in elf Tagen erledigen kann. Die Aufgabe war speziell: Ein vorhandener mathematischer Beweis sollte formalisiert werden, die Agenten arbeiteten mit einem Proof Assistant, und ein eigens gebauter Orchestrierungs-Layer zerlegte den Gesamtzustand in überprüfbare Abhängigkeiten.
Gerade diese Einschränkungen machen das Experiment für Softwareentwicklung brauchbar. Der erfolgreiche Aufbau hatte einen expliziten Projektgraphen, kleine verifizierbare Teilziele, wiederverwendbare Artefakte und einen deterministischen Prüfer. Die frühen Läufe ohne ausreichend gemeinsame Struktur scheiterten dagegen an Koordination und Zustandsverlust.
Wenn Coding-Agenten künftig größere Repositories parallel bearbeiten sollen, dürfte dieselbe Frage wichtiger werden als ein weiterer Punkt auf einem Coding-Benchmark: Wo liegt der gemeinsame, maschinenlesbare Projektzustand, und welches System entscheidet zuverlässig, dass ein Teilproblem tatsächlich erledigt ist?
Quellen: https://www.anthropic.com/research/formalizing-fermats-last-theorem https://dataconomy.com/2026/09/07/claude-completes-computer-checked-proof-fermat-last-theorem/