Fermat in Lean: geprüft, nicht gelesen

Anthropic hat am 04.09.2026 einen maschinengeprüften Beweis von Fermats letztem Satz veröffentlicht, geschrieben von Claude in der Beweissprache Lean 4. Elf Tage, weitgehend selbstständig, am Ende 29.511 Theoreme. Das Repository liegt unter Apache 2.0 auf GitHub. Wir haben es geklont und nachgezählt: 60.478 Lean-Dateien mit zusammen 13.499.380 Zeilen. Die gerundeten 13 Millionen aus der Ankündigung stimmen.

Für Mathematiker ist das eine Nachricht über Mathematik. Für uns ist es etwas anderes: ein ungewöhnlich gut dokumentierter Fall von Agenten-Output, an dem sich zwei Fragen durchspielen lassen, die im Arbeitsalltag ständig auftauchen. Wie prüft man Code, den niemand gelesen hat? Und was passiert eigentlich mit fremden Lizenzen, wenn Agenten im großen Stil Material zusammentragen?

Wir haben uns das Repository selbst angesehen. Beide Antworten sind interessant, und die zweite steht in keiner Meldung.

Der Kern-Check ist echt, und er ist drei Zeilen lang

Die naheliegende Skepsis bei formalisierten Beweisen lautet: Steht da irgendwo ein Platzhalter? In Lean heißt der sorry. Er lässt eine Beweislücke durchgehen, das Projekt baut trotzdem, und die Behauptung ist wertlos.

Anthropic begegnet dem mit einem Mechanismus, der sich nachlesen lässt. In FinalCheck.lean, dem voreingestellten Build-Ziel, steht:

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

Das ist der ganze Trick, und er funktioniert so: #print axioms listet auf, worauf ein Satz letztlich ruht. #guard_msgs vergleicht diese Ausgabe mit dem Kommentar darüber und lässt den Build scheitern, wenn sie abweicht. Die drei genannten Axiome sind Leans Standardfundament. Wäre irgendwo im Beweis ein sorry, stünde dort zusätzlich sorryAx, und der Build ginge kaputt. Dasselbe gilt für ein selbst deklariertes axiom oder für native_decide, mit dem sich Rechenschritte am Kernel vorbeischleusen lassen.

Das ist keine Absichtserklärung im Blogbeitrag, sondern eine Prüfung, die bei jedem Build mitläuft. Sie steht genau so im Repository, wir haben die Datei gelesen.

Verlassen muss man sich darauf nicht. Wir haben das Repository geklont und selbst gesucht: In den 60.478 Lean-Dateien steht kein einziges sorry, kein native_decide und keine eigene axiom-Deklaration. Die drei sorry-Treffer, die es gibt, stecken alle in verification/comparator/Challenge.lean, der Referenzdatei, die die Aussage absichtlich offen lässt und nicht zum Beweis gehört.

Dazu kommen zwei unabhängige Nachprüfungen, die Anthropic beschreibt: das Werkzeug comparator bestätigt, dass die bewiesene Aussage identisch mit einer nur aus Mathlib formulierten Referenzaussage ist, und nanoda, ein zweiter, in Rust geschriebener Lean-Kernel, hat einen Export derselben Umgebung akzeptiert. Bei nanoda haben sie vier eigene Patches eingespielt, drei davon zur Beschleunigung der Gleichheitsprüfung. Sie schreiben dazu, keiner der Patches ändere eine Typregel. Nachgerechnet haben wir das nicht.

Was der Check nicht prüft, sagt Anthropic selbst

Der ehrlichste Satz steht im README, nicht im Blogbeitrag:

"What no tool can check is that each intermediate theorem means what its name suggests; that is for the reader to judge"

Das ist der Punkt, an dem die Analogie zum Arbeitsalltag greift. Die Maschine prüft, dass die Kette hält. Sie prüft nicht, dass die Kette an der richtigen Stelle beginnt. Ein Zwischensatz namens frey_no_cofixed_large kann formal einwandfrei bewiesen sein und trotzdem etwas anderes aussagen, als der Name nahelegt. Nur der finale Satz ist gegen eine externe Referenz abgeglichen, und genau deshalb ist dieser Abgleich das Entscheidende am ganzen Aufbau.

Übersetzt: Formale Verifikation ersetzt nicht das Verstehen der Anforderung. Sie ersetzt das zeilenweise Nachlesen der Umsetzung. Das ist viel, aber es ist etwas anderes.

Nachprüfen kostet 300 GB Arbeitsspeicher

Hier wird es für die Praxis unbequem. Anthropic nennt die Anforderungen offen, und sie sind bemerkenswert:

Der Beweis ist also im strengen Sinn nachprüfbar, und praktisch können ihn nur Leute nachprüfen, die eine Maschine mit 300 GB Arbeitsspeicher danebenstehen haben. Das ist immer noch unendlich viel besser als ein Ergebnis, das man glauben muss. Es ist nur nicht dasselbe wie "jeder kann es nachrechnen".

Für Teams, die über verifizierbare KI-Ergebnisse nachdenken, ist das die realistische Erwartung: Prüfbarkeit verschiebt den Aufwand, sie schafft ihn nicht ab.

Die Copyright-Header haben es nicht überlebt

Das ist der Teil, den wir im Repository gefunden haben und der in keiner Berichterstattung vorkommt.

Der Beweis steht nicht auf der grünen Wiese. 106 Dateien enthalten Material aus fremden Projekten: 90 aus dem FLT-Projekt des Imperial College London, das Kevin Buzzard seit 2024 mit einer Community betreibt, dazu Dateien aus dem Projekt flt-regular und 23, die Mathlib-Text wiedergeben. Bei vielen davon steht in der Spalte "Extent" schlicht "whole file (100%)".

Alles steht unter Apache 2.0, hüben wie drüben. Die Lizenz erlaubt das ausdrücklich. Sie verlangt allerdings auch, dass Urhebervermerke erhalten bleiben. Und genau da ist etwas passiert. Aus ATTRIBUTION.md:

"The Lean files of this repository were assembled by AI agents and were published without their comments, so upstream headers did not survive in place."

Die Agenten haben die Kommentare entfernt, und mit den Kommentaren gingen die Copyright-Header. Anthropic hat die Zuordnung danach forensisch rekonstruiert: Sie haben alle 60.478 Lean-Dateien zeilenweise gegen die Kopien verglichen, die im Mai 2026 mit intakten Headern in ihren Arbeitsbaum gekommen waren, nach Normalisierung von Leerraum und ohne import-Zeilen. Als Treffer galt eine Datei ab fünf charakteristischen gemeinsamen Zeilen.

Das ist sauber gemacht und ungewöhnlich transparent dokumentiert, samt eines eigenen Abschnitts darüber, was die Methode nicht leisten kann. Dort steht unter anderem, dass Dateien, die nie in den Arbeitsbaum kopiert wurden, mit diesem Verfahren gar nicht auffallen können, und dass zwei Header aus den Upstream-Dateien nachgetragen werden mussten, weil die eigenen Kopien sie nicht mehr hatten.

Für uns ist das die eigentliche Lehre des Tages, und sie hat nichts mit Mathematik zu tun. Ein Agent, der Kommentare als Rauschen behandelt und beim Aufräumen entfernt, entfernt möglicherweise die Lizenzangabe gleich mit. Bei Anthropic ist es aufgefallen, weil jemand gezielt danach gesucht hat, bevor veröffentlicht wurde. In einem normalen Projekt fällt es niemandem auf.

Was davon im Arbeitsalltag zählt

Drei Dinge nehmen wir mit.

Der Abgleich gegen eine externe Referenz ist das Wertvolle. Nicht der Beweis selbst, sondern #guard_msgs mit einer erwarteten Ausgabe. Das Muster ist übertragbar: ein Test, der fehlschlägt, wenn sich eine Eigenschaft ändert, die niemand aktiv beobachtet. Wer Agenten Code schreiben lässt, sollte weniger Zeit ins Lesen der Diffs stecken und mehr in Prüfungen, die beim Build anschlagen.

Formale Verifikation lohnt dort, wo die Anforderung maschinenlesbar ist. Das ist in der Mathematik der Normalfall und in der Anwendungsentwicklung die Ausnahme. Wo es zutrifft, etwa bei Protokollen, Parsern oder Zustandsautomaten, ist der Hebel groß. Für die CRUD-Maske ist es kein Thema. Wir hatten das im Sommer schon einmal in der Praxis, als Mistrals Leanstral 1.5 echte Bugs in offenen Repos fand.

Prüft eure Agenten auf Lizenzangaben. Wenn ein Agent Dateien umformt, zusammenführt oder aufräumt, gehört die Frage, was mit fremden Headern passiert, in die Review-Checkliste. Ein grep nach Copyright-Zeilen vor dem Commit ist billig. Der Fall hier zeigt, dass es selbst dann passiert, wenn hochkompetente Leute mit klarer Lizenzlage arbeiten.

Bleibt der Punkt, an dem wir ehrlich sein müssen: Was Anthropic nicht nennt, sind die Kosten, das verwendete Modell, die Zahl der Agenten und die Zahl der Fehlversuche. Elf Tage ist eine Zeitangabe, keine Aufwandsangabe. Ohne diese Zahlen lässt sich nicht beurteilen, ob das Verfahren für andere Vorhaben in Reichweite ist oder ob hier eine sehr teure Demonstration steht.