Anthropics Lean-Beweis für Fermats letzten Satz: So lässt er sich prüfen

Wer die Schlagzeile „Claude hat Fermats letzten Satz gelöst“ liest, sollte auf ein entscheidendes Wort achten: formalisiert. Anthropic hat ein öffentliches Lean-Artefakt veröffentlicht, das den Satz nach eigenen Angaben vollständig maschinell prüft. Der mathematische Weg dahinter ist jedoch das etablierte Argument von Frey, Serre, Ribet, Wiles und Taylor-Wiles – kein neu entdeckter Beweis.

Zwei sehr unterschiedliche Aussagen

Die kurze Antwort lautet: Ja, Anthropic hat ein öffentliches Repository mit einer Lean-4-Formaliserung von Fermats letztem Satz (FLT) veröffentlicht, inklusive Anleitungen zum Bauen und Überprüfen. Die weitergehende Behauptung, Claude habe das berühmte Problem eigenständig gelöst, trifft dagegen nicht zu. Den mathematischen Durchbruch lieferten Andrew Wiles und Richard Taylor bereits vor Jahrzehnten.

FLT besagt, dass es für a^n + b^n = c^n keine Lösungen in positiven ganzen Zahlen gibt, wenn n > 2 gilt. Wiles’ Beweis erschien 1995. Anthropics Beitrag überführt diesen etablierten Beweisweg in ein maschinenprüfbares Artefakt. Historischen Kontext liefert die Ankündigung des FLT-Projekts von Lean Community.

Ein Lean-Beweis beantwortet eine andere Frage als ein informeller mathematischer Aufsatz. Er kann zeigen, dass eine präzise kodierte Aussage aus geprüften Definitionen, Abhängigkeiten und Axiomen in einer festgelegten Umgebung folgt. Er zeigt aber nicht, dass eine KI die zugrunde liegende Mathematik erfunden hat – und auch nicht automatisch, dass Theorem-Namen zu ihren Beschreibungen passen.

Was Anthropic tatsächlich veröffentlicht hat

Anthropics Forschungsbeitrag vom 4. September 2026 zufolge erzeugte Claude innerhalb von 11 Tagen die erste vollständige, durchgängig computergeprüfte Lean-Formaliserung von FLT. Der Beitrag nennt rund 13 Millionen Zeilen Lean, 30.300 bewiesene Theoreme und 29.500 davon, die im finalen Beweis verwendet wurden. Außerdem ist von ungefähr 6 Milliarden erzeugten Tokens die Rede.

Zum Einsatz kam Prove2Me, eine Plattform, die nach Anthropics Beschreibung einen gerichteten azyklischen Graphen aus Theoremen verwaltet und mehrere Agenten koordiniert. Die Formalisierung folgt laut Anthropic einer vereinfachten Darstellung des etablierten Beweiswegs von Frey, Serre, Ribet, Wiles und Taylor-Wiles.

Für die Überprüfung der Behauptung ist das öffentliche GitHub-Repository hilfreicher als die Ankündigung. Das Standardziel ist FinalCheck.lean; die zentrale Theorem-Deklaration lautet:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
  (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
  a ^ n + b ^ n ≠ c ^ n

Das Repository bezeichnet sich selbst als Forschungsartefakt, das nicht gepflegt wird und keine Beiträge annimmt. Es verwendet Lean 4.33.1 und Mathlib v4.33.0, enthält PROOF-PATH.md und stellt eine offline durchsuchbare HTML-Darstellung des Theorem- und Definitionsgraphen bereit.

Die abschließende Prüfung des Repositorys soll fehlschlagen, wenn der Beweis von einem zusätzlichen Axiom, sorry, native_decide, unsafe oder einem vergleichbaren Schlupfloch abhängt. Das macht das Artefakt überprüfbar, statt Leser auf einen Screenshot oder eine reine Zusammenfassung zu verweisen.

So lässt sich die Prüfung reproduzieren

Eine ernsthafte Überprüfung beginnt mit der festgelegten Umgebung des Repositorys – nicht damit, eine einzelne .lean-Datei in ein anderes Projekt zu kopieren. Der Verifizierungsleitfaden der Lean Community erklärt den Grund: Lean erscheint monatlich in einer neuen Version, Mathlib ändert sich häufig und Abwärtskompatibilität ist nicht garantiert.

Vor dem Build die Umgebung festnageln

Das Repository ist laut eigener Dokumentation für Linux oder macOS gedacht und benötigt elan, Git, Python, GNU coreutils sowie eine Netzwerkverbindung, damit Lake die festgelegten Abhängigkeiten herunterladen und bauen kann. Unter .lake fallen demnach etwa 67 GB an; zusätzlich entstehen ungefähr 220 GB an generierten C-Dateien, die später gelöscht werden können.

Pro parallelem Job werden laut Repository etwa 5 GB Arbeitsspeicher benötigt, wobei einzelne Module bis zu 36 GB beanspruchen. Bei 96 Jobs dauerte der Build im dort dokumentierten Lauf 5 Stunden und 32 Minuten; der maximale Speicherverbrauch lag bei 153 GB. Das sind die vom Repository gemeldeten Werte und keine Messung dieses Artikels. Sie dienen daher als Warnung für die Planung, nicht als garantierte Laufzeit.

Den passenden Prüfweg wählen

• Nur prüfen: FinalCheck.lean, PROOF-PATH.md und ATTRIBUTION.md lesen, ohne einen Build zu starten.
• Vollständiger Lean-Build: die festgelegte Toolchain verwenden und lake build ausführen.
• Unabhängige Wiederholung: nach erfolgreichem Build und Export die Comparator- und nanoda-Skripte ausführen.

Für einen frischen Klon nennt das Repository im Wesentlichen diese Abfolge:

git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt

# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build

# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh

# Run after the comparator check.
verification/nanoda/run.sh

Die einzelnen Stufen haben unterschiedliche Aufgaben:

Der Comparator ersetzt nicht die Lektüre der Theorem-Aussage. Er hilft bei der zentralen Frage, ob ein Projekt tatsächlich eine bestimmte Aussage beweist – und nicht eine abgeschwächte oder subtil abweichende Variante. Das Repository ordnet in PROOF-PATH.md benannte mathematische Schritte den Lean-Deklarationen zu. Die generierten HTML-Seiten ermöglichen es, Abhängigkeiten zu untersuchen, ohne eine Webanwendung bereitstellen zu müssen.

Für die zusätzlichen Prüfungen nennt das Repository weitere Kosten: Der Export mit 37,8 GB kann etwa 90 GB Arbeitsspeicher benötigen; der nanoda-Workflow kann während der Prüfung ungefähr 40 GB beanspruchen.

Was die Belege zeigen – und was nicht

Die Checkliste „Did you prove it?“ der Lean Community bringt die entscheidende Regel auf den Punkt: Die Kompilierung validiert die kodierte Aussage – nicht die Frage, ob ein Theorem-Name zu seiner beabsichtigten informellen Bedeutung passt. Bei diesem Artefakt verringern der Comparator und seine Nutzung von Mathlib dieses Risiko, beseitigen aber nicht die Notwendigkeit, Theorem-Deklaration und Beweispfad zu lesen.

Was das Artefakt zeigt – und was nicht

Das System hat ein formal geprüftes Lean-Artefakt von ungewöhnlichem Umfang erzeugt. Es zeigt weder einen neuen Weg zu FLT noch einen neuen elementaren Beweis oder eine eigenständige mathematische Entdeckung durch Claude.

Anthropic zufolge folgt der Beweis einer vereinfachten Version des Wiles-Wegs. Das Repository verweist zudem ausdrücklich auf bestehende Arbeiten: In ATTRIBUTION.md werden 106 Dateien genannt, die Material aus dem FLT-Projekt des Imperial College London oder aus flt-regular enthalten, daneben kommt Mathlib zum Einsatz. Diese Herkunft gehört zur korrekten Einordnung des veröffentlichten Artefakts.

Das Projekt meldet 30.300 während des Laufs bewiesene Theoreme und rund 29.500, die im finalen Beweis verwendet wurden. Das Repository spricht außerdem von 29.511 Theorem-Seiten. Dabei handelt es sich um formale Deklarationen und Abhängigkeiten, nicht um 29.511 neu entdeckte mathematische Resultate. Ein formaler Beweis macht implizite Schritte, Typen, Umwandlungen, Definitionen und Bibliotheksabhängigkeiten explizit, die ein menschlicher Beweis dem Expertenverständnis überlassen kann.

Nach Angaben des Repositorys wurden die Quellen zum Prüfen und nicht zum Lesen geschrieben: Die Namen sind maschinell erzeugt, Bezeichnungen wie P2M dienen als Pipeline-Labels, und maßgeblich ist die Aussage selbst, nicht ihr Name. Genau deshalb sind Beweispfad und Comparator ebenso wichtig wie das Schlagzeilen-Theorem.

Frühere Lean-Arbeiten sollten nicht mit der Behauptung von 2026 gleichgesetzt werden. Eine Arbeit aus dem Jahr 2023 zu Fermats letztem Satz für reguläre Primzahlen berichtete über eine vollständige, sorry-freie Formalisierung von Fall I von Kummers Theorem für reguläre Primzahlen. Gleichzeitig wurde darauf hingewiesen, dass Fall II und Kummers Lemma noch erhebliche Arbeit erforderten. Eine Überarbeitung aus dem Jahr 2025 beschrieb die Formalisierung für reguläre Primzahlen als vollständigen Beweis dieses engeren Falls.

Das Imperial/Lean-FLT-Projekt beschreibt die Formalisierung moderner Zahlentheorie als umfassenderes Infrastrukturprojekt und nicht bloß als Übertragung eines einzelnen Theorems. Anthropics Veröffentlichung ist am besten als ergänzender Beleg dafür zu verstehen, was koordinierte KI-Agenten innerhalb eines bestehenden formalen Ökosystems leisten können – nicht als Beweis dafür, dass die Ziele des früheren Projekts überflüssig geworden sind.

Welche Aussage für wen belastbar ist

Wer nur die Nachricht einordnen möchte, hat mit der offiziellen Veröffentlichung und dem Repository den Nachweis, dass das Projekt existiert. Für ein Audit sollte man den festgelegten Build reproduzieren und die Aussage prüfen. Wer KI-Forschung bewertet, muss außerdem Orchestrierung, bestehende Bibliotheken, frühere Formalisierungen und Rechenaufwand als Bestandteile des Gesamtsystems berücksichtigen.

FAQ

Hat Claude einen neuen Beweis für Fermats letzten Satz entdeckt?

Nein. Anthropics Artefakt formalisiert einen etablierten Beweisweg, der mit Frey, Serre, Ribet, Wiles und Taylor-Wiles verbunden ist. Die Leistung liegt im Umfang und in der Geschwindigkeit, mit der ein maschinenprüfbares Lean-Artefakt erstellt wurde – nicht in einer neuen mathematischen Lösung.

Beweist ein erfolgreicher Lean-Build den informellen Satz?

Er beweist, dass die kodierte Aussage aus den geprüften Abhängigkeiten in dieser Lean-Umgebung folgt. Zusätzlich muss geprüft werden, ob Aussage und Definitionen tatsächlich dem informellen Theorem entsprechen, das man behaupten möchte.

Verwendet das Repository sorry oder zusätzliche Axiome?

Das Repository gibt an, dass seine abschließende Prüfung sorry, hinzugefügte Axiome, native_decide, unsafe und mehrere verwandte Abkürzungen zurückweist. Die erwartete Axiom-Liste umfasst Leans drei Standardaxiome: propext, Classical.choice und Quot.sound. Trotzdem sollte man die Prüfung selbst reproduzieren und sich nicht allein auf die Ankündigung verlassen.

Kann ich das Ergebnis auf einem normalen Laptop reproduzieren?

Das Repository lässt sich möglicherweise untersuchen und teilweise bauen. Die vollständige Prüfung ist jedoch kein kleiner Standard-Workflow. Für den Build werden dort 153 GB maximaler Arbeitsspeicher genannt, für den Comparator bis zu 230 GB sowie ein hoher Speicherplatzbedarf. Die Hardware ist damit eine zentrale Einschränkung.

Wer die Behauptung korrekt prüfen möchte, sollte beim festgelegten GitHub-Artefakt beginnen, vor der Schlagzeile die Theorem-Deklaration lesen und das Ergebnis als umfangreiche, KI-gestützte Formalisierung bekannter Mathematik einordnen.