Es ist ein Meilenstein an der Schnittstelle von KI und Mathematik: Anthropic hat am 4. September bekannt gegeben, dass Claude die erste vollständig computerverifizierte Formalisierung von Fermats Letztem Satz erstellt hat. Das KI-System arbeitete dafür elf Tage lang weitgehend autonom und schrieb rund 13 Millionen Zeilen Code in der Beweissprache Lean — darunter 30.300 bewiesene Zwischentheoreme, von denen 29.500 in den finalen Beweis eingingen.
Was genau hat Claude geleistet?
Fermats Letzter Satz gehört zu den berühmtesten Problemen der Mathematik: Über 350 Jahre blieb unbewiesen, dass die Gleichung an + bn = cn für ganzzahlige Exponenten größer als 2 keine Lösung in positiven ganzen Zahlen hat. Erst 1995 gelang Andrew Wiles der Beweis. Ein von Menschen geschriebener Beweis ist aber noch keine maschinell prüfbare Garantie: Die Formalisierung — also die Übersetzung in eine Form, die ein Beweisassistent wie Lean Zeile für Zeile verifizieren kann — galt bislang als Mammutprojekt für viele Jahre.
Claude erledigte diese Aufgabe in elf Tagen. Zum Einsatz kam laut Anthropic ein internes Forschungsmodell, dessen Fähigkeiten etwa auf dem Niveau von Claude Fable 5.1 liegen, eingebettet in ein Multi-Agenten-System auf Basis von Claude Code. Zentrales Werkzeug war die offene Plattform Prove2Me des Anthropic-Forschers Tianyi Peng (Columbia University), die Zehntausende Teilaussagen als gerichteten Graphen verwaltet und bereits bewiesene Aussagen über natürlichsprachliche Beschreibungen auffindbar macht. Der Aufwand war enorm: rund 6 Milliarden Output-Tokens. Das fertige Beweis-Repository ist mehr als fünfmal so groß wie Mathlib, die zentrale Mathematik-Bibliothek der gesamten Lean-Community.
Einordnung von Kevin Buzzard: Gratulation mit Fußnoten
Besonderes Gewicht hat die Reaktion von Kevin Buzzard. Der Mathematiker am Imperial College London leitet ein eigenes, mit einer Million Pfund gefördertes Fünfjahresprojekt zur Formalisierung von Fermats Letztem Satz — und wurde nun von Anthropic überholt. Buzzard hat das Ergebnis geprüft und spricht von einer „außergewöhnlichen Autoformalisierungs-Leistung", die den Satz „ohne andere Annahmen als die Axiome der Mathematik" beweise.
Zugleich ordnet er nüchtern ein: Mathematisch sei nichts Neues entstanden — an der Korrektheit von Wiles' Beweis hatte ohnehin kaum jemand gezweifelt. Claudes Beweis folgt zudem der klassischen Ausarbeitung von Darmon, Diamond und Taylor aus dem Jahr 1995 und nicht dem moderneren Beweisweg, den Buzzards Projekt formalisiert. Effizient ist der Maschinencode ebenfalls nicht: Das Repository braucht etwa zwanzigmal so lange zum Kompilieren wie die gesamte Mathlib. Ein interessantes Detail nennt Anthropic selbst: Auch gescheiterte Anläufe waren produktiv — rund 7 Prozent der substanziellen Codezeilen im finalen Beweis stammen aus zunächst fehlgeschlagenen Versuchen.
Was bedeutet das für Anwender in Deutschland?
Formale Verifikation ist hierzulande kein Nischenthema: In sicherheitskritischen Branchen wie Automobilentwicklung, Bahntechnik und Medizintechnik müssen Hersteller die Korrektheit ihrer Software aufwendig nachweisen. Wenn KI-Agenten Beweise dieser Größenordnung autonom führen können, rückt maschinell geprüfte Korrektheit auch für mittelständische Entwicklungsabteilungen in Reichweite — der Beweisassistent Lean ist Open Source und kostenlos nutzbar.
Bemerkenswert ist die Kostenseite: Ein kleineres Vergleichsprojekt, die Formalisierung von Winogradows Drei-Primzahlen-Satz, gelang laut Anthropic in drei Tagen mit drei regulären Claude-Max-Abos — also ohne Rechenzentrums-Budget. Deutsche Hochschulen und Unternehmen können solche Experimente damit schon heute mit Bordmitteln starten. Spannend ist der Ansatz auch als Gegenmittel zur Halluzination: Was ein Large Language Model in Lean beweist, ist per Konstruktion korrekt — die Maschine prüft jede Zeile. Für Nachweise technischer Robustheit, wie sie der EU AI Act für Hochrisiko-Systeme verlangt, könnte formal verifizierte Software mittelfristig ein handfestes Argument werden. Entwicklungsteams, die bereits KI-Coding-Tools einsetzen, sollten das Thema Autoformalisierung deshalb auf dem Radar behalten — noch ist es Forschung, aber die Werkzeuge dafür sind frei verfügbar.