Anthropics KI formalisiert Fermats letzten Satz in Lean

Anthropic hat einen vollständigen, maschinell geprüften Beweis von Fermats letztem Satz in Lean veröffentlicht. Das Unternehmen sagt, ein internes Forschungsmodell habe ihn in 11 Tagen erzeugt. Das Ergebnis ist etwa fünfmal so groß wie Mathlib, die wichtigste offene Bibliothek formalisierter Mathematik.

Lean ist ein Beweisassistent. Man schreibt Mathematik als Code, und ein kleines Programm namens Kernel prüft jeden Schritt. Fermats letzter Satz besagt: Keine drei positiven ganzen Zahlen a, b und c erfüllen a^n + b^n = c^n, wenn n über 2 liegt. Andrew Wiles bewies ihn 1995. Bislang hatte niemand diesen Beweis so aufgeschrieben, dass ein Rechner ihn lückenlos prüfen kann.

Was tatsächlich im Repository liegt

Anthropics Forschungsbeitrag erschien am 4. September 2026. Der Code liegt auf GitHub unter der Apache-2.0-Lizenz.

Die README nennt den formalen Satz. Für positive ganze Zahlen a, b und c und jedes n von mindestens 3 ist a^n + b^n niemals gleich c^n.

Angabe	Wert
Lean-Toolchain	4.33.1
Mathlib-Revision	v4.33.0
Theoreme	29.511
Module	60.475
Bauzeit	5,5 Stunden bei 96 parallelen Jobs
Spitzenspeicher	230 GB
Exportgröße	37,8 GB

Zwei Aussagen der README wiegen schwerer als die Größe. Der Beweis enthält kein sorry, Leans Platzhalter für einen Schritt, den niemand zu Ende geführt hat. Und er ruht auf nur drei Axiomen: propext, Classical.choice und Quot.sound. Diese drei liefert Lean selbst mit. Nichts Zusätzliches wurde angenommen, um das Argument zu schließen.

Anthropic sagt, das Modell habe insgesamt 30.300 Theoreme bewiesen. Etwa 29.500 davon landeten im endgültigen Beweis. Das Unternehmen nennt 6 Milliarden Ausgabe-Token und 13 Millionen Zeilen erzeugten Lean-Code. Die Arbeit lief über Prove2Me, eine Plattform, die eine Formalisierung in kleine Aussagen zerlegt und sie parallel arbeitenden Agenten übergibt.

Wie der Beweis geprüft wurde

Es liefen drei getrennte Prüfungen, und dieser Teil lohnt das Verständnis.

Zuerst akzeptierte Leans eigener Kernel den Beweis. Danach prüfte ihn ein Werkzeug namens comparator in Version 4.33.0 in rund 15 Stunden erneut. Zuletzt verifizierte Nanoda, ein unabhängiger, in Rust geschriebener Kernel, 1.052.234 Deklarationen in etwa 30 Minuten.

Nanoda zählt, weil es keinen Code mit Lean teilt. Ein Fehler in Leans Kernel würde von Leans Kernel nicht gefunden. Eine zweite Umsetzung in einer anderen Sprache ist eine echte Kontrolle dieses Risikos.

Was Mathematiker davon halten

Kevin Buzzard leitet das Xena-Projekt. Er hält eine Förderung von 1 Million Pfund des britischen Forschungsförderers EPSRC über fünf Jahre, um genau diesen Satz zu formalisieren. In seinem Blog schrieb er, Anthropic sei zuerst dort angekommen.

Buzzard bestreitet das Ergebnis nicht. "Ich bin zu 99,9 % sicher, dass der Beweis von FLT in Ordnung ist", schrieb er. Auf Anthropics Seite nennt er die Arbeit eine "außergewöhnliche Autoformalisierungsleistung".

Er zieht aber auch eine Grenze. Die Formalisierung "folgt getreu der frühen Literatur zum Beweis und fügt nichts hinzu", schrieb er. Sie hält sich an die Darstellung von Darmon, Diamond und Taylor aus dem Jahr 1995 zum Wiles-Argument. Neue Mathematik wurde hier nicht gefunden. Neu ist, dass die alte Mathematik jetzt maschinell prüfbar ist.

Buzzard merkt an, dass der Beweis Primzahlen ab 17 abdeckt. Kleinere irreguläre Primzahlen waren bereits von anderen formalisiert worden. Ein Kommentator seines Beitrags, David Jao, bezifferte die API-Kosten des Laufs auf etwa 300.000 US-Dollar.

Was das für Entwickler bedeutet

Wer Lean schreibt, kann das Repository klonen, sollte aber zuerst die Hardware prüfen. Eine Bauzeit von 5,5 Stunden bei 96 Jobs, mit 230 GB Speicherspitze, schließt fast jeden Laptop aus. Lesen Sie stattdessen die erzeugte HTML-Dokumentation. Sie ist 390 MB groß und braucht keinen Build.

Die übertragbare Lehre ist nicht, dass ein Modell 13 Millionen Zeilen schrieb. Sie ist, dass niemand sie lesen musste. Ein Kernel entschied in Minuten über die Korrektheit, ohne dem Erzeuger zu vertrauen.

Das funktioniert nur dort, wo ein Prüfer existiert. Lean hat einen. Ihr Webdienst nicht. Bevor Sie das als Vorlage nehmen, fragen Sie, was in Ihrem Stack die Rolle des Kernels übernimmt. Ein Typsystem, ein Property-Test oder ein Fuzzer sind die üblichen Kandidaten.

Wer KI-geschriebenes Lean prüft, kommt mit zwei mechanischen Kontrollen weit. Suchen Sie nach sorry, und lassen Sie sich die Axiomliste ausgeben. Anthropics eigene Behauptung ruht auf diesen zwei Fakten, und beide sind billig selbst zu bestätigen.

Der Kostenunterschied ist das Letzte, was auffällt. Den Beweis zu erzeugen kostete 11 Tage und Milliarden Token. Ihn in einer anderen Sprache nachzuprüfen kostete eine halbe Stunde. Anthropic hat Forschungsmodelle schon zuvor auf Laborarbeit gerichtet, und dasselbe Muster gilt hier. Erzeugen ist teuer. Prüfen ist billig.