Claude formalisiert Fermats letzten Satz: Was der Lean-Beweis zeigt

Was Anthropic am 4. September veröffentlicht hat

Anthropic hat einen vollständigen, maschinengeprüften Beweis von Fermats letztem Satz in Lean 4 veröffentlicht. Der berühmte Satz besagt, dass es für natürliche Zahlen n größer als 2 keine positiven ganzen Zahlen a, b und c mit a hoch n plus b hoch n gleich c hoch n gibt. Andrew Wiles und Richard Taylor schlossen den klassischen mathematischen Beweis in den 1990er-Jahren ab; neu ist hier dessen umfassende formale Codierung.

Anthropic bezeichnet das Ergebnis als ersten vollständigen, computergeprüften Beweis des Satzes. Diese Prioritätsbehauptung ist eine Herstellerangabe. Nachvollziehbar ist dagegen unmittelbar, dass das Unternehmen den Quellcode, den genauen Lean-Satz, den Prüfpfad und die Verifikationsdateien offen auf GitHub bereitstellt.

Ereignisdatum: 4. September 2026. Claude entdeckte keinen neuen Satz, sondern übersetzte einen bestehenden mathematischen Beweis in eine Form, die Beweisprüfer kontrollieren können.

Wie Claude und Prove2Me den Beweis zerlegten

Laut Anthropic arbeiteten Dutzende Claude-Agenten an Definitionen, Zwischensätzen und immer anspruchsvolleren Teilbeweisen. Die erfolgreiche Versuchsanordnung nutzte Prove2Me, eine offene Plattform für kollaborative Formalisierung, zusammen mit einem auf Claude Code basierenden Multi-Agenten-Harness. Ein gerichteter Graph hielt Abhängigkeiten zwischen Sätzen fest, half bei der Aufgabenverteilung und verringerte den Kontextverlust zwischen den Agenten.

Die menschliche Steuerung bestand nach Darstellung des Unternehmens vor allem aus gelegentlichen Hinweisen auf hochrangige mathematische Prioritäten. Der Beweis folgt einer vereinfachten Darstellung des Wiles-Ansatzes von Henri Darmon, Fred Diamond und Richard Taylor und baut auf vorhandenem offenem Lean-Material auf. Er ist damit weder aus dem Nichts entstanden noch ein Beleg dafür, dass das Modell die gesamte Mathematik ohne menschliche Vorarbeit entwickelt hat.

13 Millionen Zeilen und sechs Milliarden Output-Tokens

Anthropic beziffert den finalen Umfang auf rund 13 Millionen Zeilen Lean-Code. Im Verlauf seien 30.300 Sätze bewiesen worden, von denen ungefähr 29.500 in den finalen Beweis eingingen. Der erfolgreiche Lauf dauerte knapp zwei Wochen beziehungsweise rund elf Tage.

Die Agenten verbrauchten laut Unternehmen etwa sechs Milliarden Output-Tokens eines internen, allgemeinen Forschungsmodells, das grob mit Claude Fable 5.1 vergleichbar sei. Diese Angabe macht zugleich eine wichtige Grenze sichtbar: Der Lauf ist kein typischer Chatbot-Dialog und lässt sich aus der Veröffentlichung nicht auf Kosten oder Erfolgschancen eines normalen Claude-Abonnements übertragen.

Die Angaben zu Laufzeit, Tokenverbrauch und Modellvergleich stammen von Anthropic. Ein unabhängig reproduzierter Kostenvergleich liegt in den veröffentlichten Quellen nicht vor.

Was die maschinelle Prüfung konkret bestätigt

Das Repository pinnt Lean 4.33.1 und Mathlib v4.33.0. Sein Standardziel FinalCheck.lean prüft, dass der Satz nur auf Leans drei Standardaxiomen propext, Classical.choice und Quot.sound beruht. Nach Angaben im Repository wurden alle 60.475 Module aus einer frischen Umgebung gebaut und jede Deklaration vom Lean-Kernel geprüft.

Zusätzlich verglich leanprover/comparator die bewiesene Aussage mit einer unabhängig formulierten Herausforderung auf Basis von Mathlib. Ein zweiter, in Rust geschriebener Kernel namens nanoda akzeptierte laut Verifikationsprotokoll 1.052.234 Deklarationen ohne Fehler. Für nanoda verwendete das Team vier offengelegte Leistungs-Patches; das Repository erklärt, keiner davon verändere die Typregeln.

• Der Quellcode enthält im Beweispaket keine Platzhalter wie sorry oder zusätzliche axiom-Deklarationen.
• Die geprüfte Endaussage verwendet natürliche Zahlen und stimmt laut comparator mit Mathlibs Formulierung von Fermats letztem Satz überein.
• PROOF-PATH.md ordnet die mathematischen Schritte den jeweiligen Lean-Sätzen zu.
• Die verwendeten Versionen und Verifikationsskripte sind im Repository festgehalten.

Was damit nicht automatisch bewiesen ist

Ein Beweisassistent prüft, ob die codierte Schlusskette nach seinen Regeln aus den angegebenen Axiomen folgt. Er bewertet nicht, ob automatisch erzeugte Namen oder Kommentare die mathematische Bedeutung gut beschreiben. Das Repository weist selbst darauf hin, dass bei einem Widerspruch zwischen Name und Aussage immer die formale Aussage maßgeblich ist.

Auch die Bezeichnungen erster vollständiger oder größter Lean-Beweis sind keine Ergebnisse des Kernels. Sie stammen von Anthropic und müssen wissenschaftshistorisch separat beurteilt werden. Das offene Artefakt verbessert die Prüfbarkeit erheblich, ersetzt aber weder eine verständliche mathematische Darstellung noch die unabhängige Begutachtung durch Fachleute.

Warum die Orchestrierung wichtiger ist als ein einzelner Prompt

Anthropic berichtet auch von gescheiterten Anläufen. Frühe Agentengruppen verloren den gemeinsamen Projektzustand und koordinierten ihre Arbeit zunehmend schlechter. Teile dieser Versuche blieben zwar im Endergebnis erhalten, den Durchbruch brachte aber erst die strukturierte Zerlegung mit gemeinsamem Abhängigkeitsgraphen, Suchfunktion und wiederverwendbaren Zwischensätzen.

Das ist für KI-Agentensysteme mindestens so interessant wie der mathematische Rekordanspruch. Bei langen Aufgaben entscheidet nicht nur die Modellleistung, sondern auch eine Architektur, die Zustände stabil speichert, Arbeitspakete klein hält, Ergebnisse automatisch prüft und fehlgeschlagene Pfade sichtbar macht.

Warum das Ergebnis für KI und Forschung relevant ist

Große mathematische Formalisierungen galten bislang als langwierige Arbeit, weil jeder informelle Gedankenschritt präzise in Definitionen und Beweisobjekte übersetzt werden muss. Der veröffentlichte Lauf zeigt, dass Agententeams diese Arbeit bei vorhandener mathematischer Grundlage und maschinellem Feedback stark beschleunigen können.

Besonders wichtig ist die Verbindung von Generierung und deterministischer Kontrolle. Das Sprachmodell schlägt Beweisschritte vor, aber der Kernel entscheidet nach festen Regeln, ob sie gelten. Dieses Muster ist nicht direkt auf jede Wissensarbeit übertragbar; es zeigt jedoch, welchen Vorteil KI-Systeme in Bereichen haben, in denen Ergebnisse formal testbar und Zwischenprodukte wiederverwendbar sind.

So lässt sich die Veröffentlichung selbst prüfen

Interessierte sollten mit der exakten Aussage in Theorems/Thm_fermat_last_theorem.lean und dem Kontrollziel FinalCheck.lean beginnen. PROOF-PATH.md bietet danach eine lesbarere Route durch die zentralen mathematischen Stationen. Unter verification dokumentiert das Projekt die comparator- und nanoda-Prüfungen.

Wer den Build reproduzieren will, sollte die gepinnten Lean- und Mathlib-Versionen, die Hardwareanforderungen und die dokumentierten Prüfschritte unverändert festhalten. Eine erfolgreiche Wiederholung bestätigt die technische Verifikation; eine fachliche Bewertung des Aufbaus und seiner Beziehung zur mathematischen Literatur bleibt eine eigene Aufgabe.

• Exakte Endaussage statt Projektüberschrift prüfen
• Gepinnte Lean- und Mathlib-Versionen kontrollieren
• FinalCheck, comparator und zweiten Kernel getrennt betrachten
• Herkunft übernommener Lean-Dateien in NOTICE und ATTRIBUTION prüfen
• Herstellerangaben und selbst reproduzierte Ergebnisse auseinanderhalten

Die MindrAils-Einordnung

Die eigentliche Nachricht ist nicht, dass ein Sprachmodell Fermats letzten Satz neu gelöst hätte. Bemerkenswert ist, dass ein Agentensystem eine sehr große bestehende mathematische Argumentation in kurzer Zeit in maschinenprüfbaren Code überführt und das Ergebnis samt Prüfpfad offenlegt.

Der Fall ist deshalb ein starkes Beispiel für verantwortbare KI-gestützte Forschung: ehrgeizige Generierung, klare Versionsbindung, deterministische Prüfung und ein zugängliches Artefakt. Gleichzeitig bleiben die Rekordbehauptungen, der enorme Ressourcenverbrauch und die fehlende unabhängige Reproduktion gute Gründe, das Ergebnis präzise statt triumphal einzuordnen.