Bewiesen ist Fermats letzter Satz seit 1995, doch nun hat das KI-Unternehmen Anthropic nach eigenen Angaben erstmals eine vollständig computerverifizierte Fassung dieses Beweises vorgelegt. Ein Schwarm von Claude-Agenten soll sie in elf Tagen im Beweisassistenten Lean geschrieben haben: 13 Millionen Zeilen Code, 29.500 Zwischentheoreme. Die Fachwelt hatte dafür Jahre veranschlagt. Der Code liegt offen, eine unabhängige Bewertung steht weitgehend aus.

Es geht hier ausdrücklich nicht um neue Mathematik. Fermats letzter Satz – die Gleichung xⁿ + yⁿ = zⁿ hat für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen – wurde 1995 von Andrew Wiles auf 129 Seiten bewiesen und gilt in der Fachwelt seither als gesichert. Was fehlte, war die Formalisierung: die Übersetzung dieses Beweises in eine Form, die ein Computer Schritt für Schritt automatisch nachprüfen kann. Genau das soll Claude nun geleistet haben, wie Anthropic in einem Beitrag zur Formalisierung von Fermats letztem Satz schreibt.

Werkzeug der Wahl war wie schon bei früheren KI-Beweisen der Beweisautomat Lean. Dabei handelt es sich um eine Programmiersprache und ein Prüfsystem in einem. Mathematische Aussagen und ihre Herleitungen werden als Code notiert, den Lean anschließend gegen ein festes logisches Regelwerk prüft. Geht die Kette nicht lückenlos auf, kompiliert der Beweis schlicht nicht. Vertrauen muss man am Ende nur noch dem kleinen Kern des Systems und dessen Axiomen – nicht mehr der Sorgfalt einzelner Gutachter.

Der Aufwand dafür ist allerdings enorm: Ein für Menschen geschriebener Beweis überspringt viele als offensichtlich geltende Schritte und baut auf Jahrhunderten publizierter Arbeit auf. Lean muss jeden einzelnen Schritt sehen, egal wie trivial, und kann dabei nur auf den vergleichsweise winzigen Teil der Mathematik zurückgreifen, der bereits formalisiert vorliegt. Gesammelt ist dieser Bestand in Mathlib, der zentralen Community-Bibliothek formalisierter Mathematik.

Der Anthropic-Forscher Tianyi Peng, dessen Gruppe an der Columbia University Werkzeuge für KI-gestützte Formalisierung entwickelt, wollte prüfen, ob Claude beim Formalisieren von Fermats letztem Satz (Fermat’s Last Theorem, FLT) überhaupt Fortschritte macht. Das Ergebnis habe die Erwartungen übertroffen: In elf Tagen habe Claude weitgehend autonom die erste durchgängige, computergeprüfte Fassung produziert. Herausgekommen seien 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Dutzende Claude-Agenten hätten dabei zusammengearbeitet, um Konzepte zu definieren, Zwischentheoreme zu beweisen und damit immer schwierigere Aussagen zu belegen.

Formalisiert wurde nach diesen Angaben eine vereinfachte Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Menschlicher Input habe sich auf gelegentliche High-Level-Anweisungen Pengs beschränkt.

Wie belastbar ist die Formalisierung?

Nach Anthropics Darstellung wurde das Ergebnis von Lean geprüft und nutzt nur Leans drei Standardaxiome, und ein Komparator bestätigte, dass die Theorem-Aussage mit Mathlibs eigener FLT-Formulierung übereinstimmt. Der vollständige Beweis liegt samt schriftlichem Walkthrough im GitHub-Repository von Anthropic. Ob ein Lean-Beweis kompiliert, kann jeder Dritte feststellen.

Die Prüfung adaptiert Teile aus dem von Kevin Buzzard geleiteten FLT-Projekt am Imperial College London sowie aus dem flt-regular-Projekt; Lean und Mathlib gehen auf Beiträge von Hunderten Mathematikern zurück. Buzzards 2024 gestartetes Community-Projekt ist bis September 2029 gefördert; allein der Blueprint des Projekts umfasst 86 Seiten.

Buzzard hat die Arbeit begutachtet und spricht von einem großen Schritt hin zur automatischen Formalisierung der modernen mathematischen Literatur. Buzzard hat den Code inzwischen selbst kompiliert und den Komparator laufen lassen – er hält stand. Mathematisch liefere die Arbeit aber nichts Neues, die Formalisierung folge nur der frühen Literatur zum Beweis, schreibt er in seinem Blog Xena Project.

Der Weg zum Ergebnis

Interessant zu lesen ist, dass zunächst mehrere Anläufe scheiterten. Zwar hätten die ersten Agenten-Teams Teilerfolge erzielt, den Überblick über den Projektzustand aber schnell verloren und aufgehört, effektiv zusammenzuarbeiten. Der Durchbruch kam laut Anthropic erst mit dem Wechsel auf Prove2Me, eine offene Plattform zur Formalisierung von Mathematik, die Peng und Kollegen an der Columbia University entwickelt haben. Sie pflegt einen gerichteten azyklischen Graphen von Theoremaussagen, anhand dessen die Agenten entscheiden, welche Beweise sie als Nächstes angehen. Dies soll Speicherdegradation entgegenwirken und Parallelarbeit ermöglichen.

Der Erfolg hängt also erkennbar nicht am Modell allein, sondern an der unterstützenden Infrastruktur und den Steuerungsmechanismen drumherum. Das Agententeam verbrauchte laut Anthropic rund sechs Milliarden Output-Token, woraus sich Kosten zwischen 100.000 und 300.000 US-Dollar hochrechnen lassen – eine Summe nennt Anthropic selbst nicht. Dass es kleiner geht, soll ein Nebenexperiment zeigen – mit drei privaten Claude-Max-Abos formalisierten Agenten über Prove2Me in drei Tagen den Drei-Primzahlen-Satz von Winogradow.

Die Meldung reiht sich in eine Serie von KI-Erfolgen ein, deren Bilanz gemischter ist, als die Schlagzeilen nahelegen. Bereits 2024 erreichten die DeepMind-Modelle AlphaProof und AlphaGeometry 2 bei der Internationalen Mathematik-Olympiade Silbermedaillenniveau mit vier von sechs gelösten Aufgaben.

Im April 2026 löste ein 23-Jähriger mit einem einzigen Prompt an GPT-5.4 Pro ein 60 Jahre altes Erdős-Problem – bemerkenswert vor allem wegen des Lösungswegs über Markov-Ketten; auch dieser Beweis wurde in Lean formal verifiziert. Kurz darauf widerlegte ein internes OpenAI-Reasoning-Modell eine 80 Jahre alte Annahme zum „planar unit distance“-Problem – wobei die prüfenden Mathematiker anmerkten, dass sich die Argumentation entscheidend auf Ideen stütze, die zumindest im Nachhinein anderen Autoren zugeschrieben werden könnten.

Hintergrund: Warum der Satz so lange widerstand

Faszinierend an Fermats letztem Satz ist, dass er zwar einfach zu verstehen ist, der Beweis aber mehr als 350 Jahre lang auf sich warten ließ. Fermat war hauptberuflich Jurist und notierte um 1640 an den Rand eines Buches, er habe einen wunderbaren Beweis gefunden, der Rand sei aber zu schmal. Wie ernst es die Fachwelt mit der Suche meinte, zeigt der Wolfskehl-Preis: 1908 wurden 100.000 Goldmark ausgelobt, allein im ersten Jahr gingen mehr als 600 fehlerhafte Beweisversuche ein.

Andrew Wiles kam als Zehnjähriger über ein Buch zum Problem und griff es erst wieder auf, als Gerhard Frey 1986 die Verbindung zur Taniyama-Shimura-Vermutung aufzeigte. Wiles präsentierte im Juni 1993 seinen vermeintlich korrekten Beweis. Zwei Monate nach Beginn der Prüfung deckte die Rückfrage eines Gutachters eine kritische Lücke auf. Wiles brauchte ein weiteres Jahr – zuletzt mit seinem früheren Studenten Richard Taylor – und stand kurz vor dem Aufgeben, als er erkannte, dass ein zuvor verworfener Ansatz die Lösung war. Genau diese Episode ist das stärkste Argument für Formalisierung – und der Grund, warum das Vorhaben überhaupt in Angriff genommen wurde.

(vza)