Forschung · Formale Verifikation
Elf Tage, 13 Millionen Zeilen Lean: Claude hat Fermats letzten Satz maschinell nachprüfbar gemacht — die Fachwelt zieht drei Fußnoten ein
Am Freitag hat Anthropic einen Forschungsbericht veröffentlicht, der in der Mathematik-Gemeinde seither diskutiert wird: Ein Claude-Modell hat über elf Tage weitgehend selbstständig einen vollständigen, maschinell geprüften Beweis von Fermats letztem Satz in der Beweissprache Lean geschrieben. Wichtig für die Einordnung: Der Rechenlauf selbst lief bereits im August und endete in der Nacht zum 18. August — die Veröffentlichung kommt gut zwei Wochen später, was Anthropic auch selbst so schreibt („last month“).
Fermats letzter Satz ist die Behauptung, dass die Gleichung an + bn = cn für positive ganze Zahlen und n größer als 2 keine Lösung hat. Pierre de Fermat notierte sie um 1637 an den Rand eines Buches; bewiesen wurde sie erst 1995 von Andrew Wiles — auf 129 Seiten, die Jahrzehnte moderner Zahlentheorie zu einer einzigen Kette verknüpfen. Genau das ist das Problem: Eine solche Kette prüft kein Mensch in vertretbarer Zeit lückenlos nach, und Wiles selbst musste nach einer entdeckten Lücke ein Jahr nachbessern. Ein Beweisassistent wie Lean nimmt einem diese Arbeit ab — er akzeptiert einen Schritt nur, wenn er formal aus dem Vorangegangenen folgt.
Die Zahlen des Laufs sind bemerkenswert: rund 13 Millionen Zeilen Lean-Code, 30.300 bewiesene Theoreme, davon 29.500 im finalen Beweis verwendet, und etwa sechs Milliarden erzeugte Token. Zum Vergleich zieht Anthropic Mathlib heran, die gemeinschaftlich gepflegte Standardbibliothek des Lean-Ökosystems: Der Beweis ist mehr als fünfmal so groß. Das eingesetzte Modell benennt Anthropic nicht, sondern beschreibt es als internes Forschungsmodell, das ungefähr mit Claude Fable 5.1 vergleichbar sei.
Der eigentliche Fortschritt steckt aber nicht im Modell, sondern in der Organisation. Frühere Anläufe scheiterten daran, dass die Agenten über Tage den Überblick über den Projektstand verloren. Erst der Umstieg auf Prove2Me brachte den Durchbruch — eine offene Plattform, die den Beweis als gerichteten azyklischen Graphen von Theorem-Aussagen führt, aus dem jeder Agent abliest, welcher Teilbeweis als Nächstes dran ist. Entwickelt hat sie eine Gruppe um Tianyi Peng, der zugleich für Anthropic forscht und an der Columbia University eine Gruppe für KI-gestützte Formalisierung leitet; das zugehörige Papier steht seit dem 28. August auf arXiv.
Die interessanteste Reaktion kommt von dem, der am meisten Grund zur Verstimmung hätte. Kevin Buzzard vom Imperial College London leitet seit 2024 ein mit einer Million Pfund über fünf Jahre gefördertes Gemeinschaftsprojekt mit demselben Ziel. Er hat Anthropics Code kompiliert, mit einem Abgleichprogramm gegen Mathlibs eigene Formulierung des Satzes geprüft — damit nicht versehentlich eine andere, leichtere Aussage bewiesen wurde — und schreibt in seinem Blog nüchtern: „I've compiled the code base and run comparator on it — it checks out.“ An der technischen Kernaussage zweifelt niemand.
Buzzard zieht aber drei Fußnoten ein, die in der Ankündigung fehlen. Erstens ist die Arbeit keine Neuentwicklung aus dem Nichts: Anthropic schreibt selbst, der Beweis übernehme Teile aus Buzzards Imperial-Projekt und aus dem Gemeinschaftsprojekt flt-regular. Zweitens deckt Anthropics neues Argument nur Primzahlen ab 17 ab; die Fälle 3, 5, 7, 11 und 13 stützen sich auf jene vorbestehende Formalisierung. Der vollständige Beweis ist also eine Kombination aus neuem Beitrag und jahrelanger Gemeinschaftsarbeit — eine Einschränkung, die außer bei Buzzard nirgends auftaucht. Drittens, und das ist die wichtigste: Mathematisch ist nichts Neues entstanden. „The formalization just faithfully follows the early literature on the proof and adds nothing“, schreibt Buzzard; er sei seit jeher zu 99,9 Prozent sicher gewesen, dass Wiles' Beweis stimmt. Formalisiert wurde auch nicht Wiles' Originalarbeit, sondern eine didaktisch aufbereitete Fassung von Darmon, Diamond und Taylor aus demselben Jahr.
Was bleibt, ist trotzdem beachtlich, und Buzzard sagt das auch: Der Lauf schließt die letzte offene Aufgabe auf Freek Wiedijks zwanzig Jahre alter Liste von hundert Formalisierungs-Herausforderungen und zeigt, dass sich tausende Seiten Fachliteratur in elf Tagen maschinell nachprüfbar machen lassen. Sein eigenes Projekt hält er deshalb nicht für erledigt — es verfolgt einen moderneren Beweisweg und soll die Bausteine in Mathlib zurückspeisen, was Anthropic seiner Vermutung nach nicht tun wird. Eine Angabe fehlt in der Ankündigung ganz: die Kosten. In der Kommentarspalte seines Blogs rechnen Fachleute aus sechs Milliarden Ausgabe-Token Beträge im niedrigen sechsstelligen Dollarbereich hoch — belastbar ist das nicht. Buzzard merkt nur an, er habe für fünf Jahre eine Million Pfund bekommen, Anthropic elf Tage gebraucht, und er frage sich, ob dabei nicht mehr Geld geflossen sei.
Für unsere Leserinnen und Leser ist der Vorgang die Fortschreibung einer Linie, die wir seit dem Sommer verfolgen: Am 12. August berichteten wir, wie ein unveröffentlichtes Claude-Modell eine 150 Jahre alte Schranke von 41,6 auf 67,2 Prozent hob, und ordneten am selben Tag in unserer Reportage ein, warum formale Verifikation plötzlich bezahlbar wird. Neun Tage später haben wir am Beispiel eines Mathematik-Erfolgs von OpenAI gezeigt, wie schnell solche Meldungen ihren Nenner verlieren. Der FLT-Lauf ist der bislang größte Beleg dafür, dass diese Arbeitsteilung funktioniert — und zugleich das klarste Beispiel dafür, dass sie nur dort funktioniert, wo ein Prüfer jeden Zwischenschritt sofort und kostenlos beurteilt. Was das für Aufgaben außerhalb der Mathematik bedeutet, ist das Thema unserer Reportage in dieser Ausgabe.
- Anthropic — Formalizing Fermat's Last Theorem
- Kevin Buzzard (Xena Project) — FLT: Anthropic has beaten me to it
- GitHub — anthropics/fermats-last-theorem
- arXiv — Prove2Me: An Open Collaborative Platform for Scaling Math Formalization
- SiliconANGLE — Anthropic uses Claude to formalize proof of Fermat's Last Theorem