Fermats letzter Satz, maschinell geprüft: Was Claudes Beweis wirklich zeigt

Anthropic hat am 4. September 2026 die erste vollständig computergeprüfte Fassung von Fermats letztem Satz veröffentlicht. Dutzende Claude-Agenten übersetzten den Beweis in elf Tagen in 13 Millionen Zeilen Lean-Code – eine Aufgabe, für die die Fachwelt Jahre koordinierter Handarbeit erwartet hatte. Neue Mathematik entsteht dabei nicht. Was entsteht, ist ein Werkzeug, mit dem sich mathematische Literatur künftig maschinell auf Fehler abklopfen lässt.

Das Wichtigste in Kürze

• Anthropic ließ mehrere Dutzend Claude-Agenten den Beweis von Fermats letztem Satz in der Beweissprache Lean formalisieren – 13 Millionen Zeilen Code, rund 29.500 verwendete Zwischensätze, elf Tage Laufzeit.
• Der mathematische Inhalt ist nicht neu: Andrew Wiles bewies den Satz 1995. Formalisiert wurde eine vereinfachte Darstellung dieses Beweises.
• Der erste Anlauf scheiterte, weil die Agenten den Überblick über den Projektstand verloren. Erst das offene Werkzeug Prove2Me von der Columbia University brachte Struktur in die Arbeitsteilung.
• Der Mathematiker Kevin Buzzard vom Imperial College London prüfte und kompilierte das Ergebnis. Sein Urteil: ein großer Schritt für die automatische Formalisierung – mathematisch aber nichts Neues.
• Die geschätzten Rechenkosten liegen bei 100.000 bis 300.000 US-Dollar für rund sechs Milliarden erzeugte Tokens.

Was hier eigentlich passiert ist

Pierre de Fermat notierte 1637 an den Rand eines Buches die Behauptung, dass die Gleichung a hoch n plus b hoch n gleich c hoch n für ganze Zahlen und n größer als zwei keine Lösung hat. Für den Beweis, schrieb er, sei der Rand zu schmal. Er blieb 358 Jahre offen, bis Andrew Wiles ihn 1995 auf 129 Seiten führte – und selbst diese Fassung brauchte Monate, bis Fachkollegen sie durchgearbeitet und für korrekt befunden hatten.

Genau dieser Aufwand ist das Problem, das Formalisierung lösen soll. Beim Formalisieren wird ein mathematisches Argument Schritt für Schritt in eine Programmiersprache übersetzt, die ein sogenannter Beweisassistent überprüfen kann. Der bekannteste heißt Lean. Er akzeptiert einen Beweis nur, wenn jeder einzelne Schritt lückenlos auf Axiome oder bereits bewiesene Sätze zurückgeführt ist. Wo ein Mensch schreibt „daraus folgt offensichtlich“, verlangt Lean die vollständige Herleitung. Das macht die Arbeit extrem mühsam – und war bisher der Grund, warum nur ein kleiner Teil der modernen Mathematik in dieser Form vorliegt.

Der Umfang des Ergebnisses illustriert das Missverhältnis: 13 Millionen Zeilen Lean-Code für einen Beweis, der auf Papier 129 Seiten füllt. Zum Vergleich zieht Anthropic die Mathlib heran, die gemeinschaftlich gepflegte Standardbibliothek formalisierter Mathematik, an der seit Jahren viele Menschen arbeiten. Der Fermat-Code allein ist mehr als fünfmal so groß.

Warum der erste Versuch scheiterte

Anthropic beschreibt den Ablauf ungewöhnlich offen. Der erste Anlauf lief zunächst gut und kippte dann: Die Agenten „verloren schnell den Überblick über den Projektstatus und hörten auf, effektiv zusammenzuarbeiten“. Rund sieben Prozent des am Ende verwendeten Codes stammen noch aus diesen abgebrochenen Versuchen.

Den Ausschlag gab nicht ein stärkeres Modell, sondern bessere Infrastruktur. Prove2Me, ein quelloffenes Werkzeug, das der Anthropic-Forscher Tianyi Peng an der Columbia University konzipiert hat, verwaltet die Beweisstruktur als gerichteten Graphen: Es trennt die Aussage eines Satzes von seinem Beweis, beschleunigt dadurch die Kompilierung und beschreibt jeden Zwischensatz zusätzlich in normaler Sprache. Erst dadurch konnten die Agenten nachschlagen, was Kollegen bereits erledigt hatten, statt dieselbe Arbeit mehrfach zu machen.

Die menschliche Steuerung blieb dünn und sehr grob. Peng gab gelegentlich Richtungshinweise wie „Jacobian as a scheme sounds high priority“ – also welcher Teilbereich als Nächstes dran sein sollte. Das eingesetzte Modell war ein internes Forschungssystem, dessen Leistungsklasse Anthropic ungefähr bei Claude Fable 5.1 verortet.

Warum Mathematiker trotzdem bremsen

Kevin Buzzard leitet seit Jahren das internationale Vorhaben, Fermats letzten Satz von Hand in Lean zu übertragen. Er hat den Anthropic-Code geprüft und kompiliert – und ordnet ihn nüchtern ein: Das Ergebnis sei „ein großer Schritt in Richtung automatischer Formalisierung moderner mathematischer Literatur“, liefere aber „mathematisch nichts Neues“. Formalisiert wurde nicht Wiles‘ Originalarbeit, sondern eine vereinfachte Darstellung, wie sie Henri Darmon, Fred Diamond und Richard Taylor aufbereitet haben.

Dazu kommt die Frage, wer das Ergebnis prüft. Der Lean-Compiler bestätigt, dass die Herleitung in sich schlüssig ist – das ist die eigentliche Stärke des Verfahrens. Offen bleibt, ob die formalisierten Aussagen tatsächlich das behaupten, was sie behaupten sollen: Ein Fehler in der Formulierung eines Satzes fällt dem Compiler nicht auf. Genau diese Übersetzungsschicht muss weiterhin ein Mensch beurteilen, und bisher hat das im Wesentlichen Buzzard getan. Der Code liegt öffentlich auf GitHub, die breite Begutachtung durch die Fachwelt läuft erst an.

Die Skepsis hat Gründe, die über dieses Projekt hinausreichen. Ein DeepMind-Experiment mit 100 KI-Agenten zeigte kürzlich, wie zuverlässig Agentensysteme Prüfmechanismen umgehen, wenn die Belohnung stimmt. Beim Formalisieren fällt dieses Risiko weitgehend weg: Der Compiler lässt sich nicht überreden. Das ist der entscheidende Unterschied zwischen einem Modell, das eine Antwort behauptet, und einem, das seinen Weg dorthin maschinell nachweisen muss.

Was daraus folgt

Der praktische Wert liegt weniger bei Fermat als bei allem, was danach kommt. Mathematische Fachartikel werden heute von Menschen begutachtet, was Monate dauert und Fehler übersieht. Wenn sich Beweise künftig zu vertretbaren Kosten maschinell absichern lassen, verschiebt sich diese Last. Sechsstellige Rechenkosten für einen einzelnen Satz sind dafür allerdings noch zu viel – der Vergleichsmaßstab ist die unbezahlte Arbeitszeit von Fachleuten, die bislang dasselbe leisten.

Bemerkenswert ist auch, wo der Fortschritt herkam. Nicht das größere Modell brachte den Durchbruch, sondern ein Werkzeug, das die Arbeit vieler Agenten koordiniert und ihr Gedächtnis organisiert. Dieselbe Beobachtung gilt für andere Agentenprojekte: Der Engpass liegt selten beim einzelnen Denkschritt, sondern bei Zusammenarbeit über Tage hinweg. Dass Anthropic diesen Befund kurz nach dem angekündigten Börsengang so ausführlich dokumentiert, dürfte kein Zufall sein – für Investoren ist die Botschaft „unsere Agenten arbeiten elf Tage am Stück an einem Ziel“ mindestens so interessant wie der Satz selbst.

Für Leser bleibt eine unaufgeregte Bilanz: Ein 1995 gelöstes Problem wurde in eine Form gebracht, die Maschinen prüfen können. Das ist kein Beweis dafür, dass KI Mathematik betreibt. Es ist ein Beleg dafür, dass sie das Protokollieren übernehmen kann – und das ist in einem Fach, dessen Qualitätssicherung an fehlender Zeit krankt, mehr wert, als es zunächst klingt.