Fermats Letzter Satz in Lean 4 verifiziert

Das Dienstag-Spezial dieser Rubrik behandelt ein Ereignis, das gleichermaßen der Mathematik wie der Softwareentwicklung angehört: die vollständige Formalisierung von Fermats Letztem Satz in Lean 4. Das von Anthropic veröffentlichte Repository enthält einen maschinengestützten Beweis, aufgebaut auf Mathlib, mit Lean 4.33.1 Toolchain und Mathlib v4.33.0 gepinnt via Commit in lakefile.lean, wie im offiziellen Repository^[1] dokumentiert.

Was sich technisch geändert hat

Das formalisierte Argument folgt der klassischen Trajektorie: Frey, Serre, Ribet, Wiles und Taylor-Wiles. Die Datei PROOF-PATH.md listet jeden Schritt zusammen mit dem entsprechenden Lean-Theorem auf, während der Ordner html/ den gesamten Beweis als offline navigierbare Webseiten darstellt.

Der zentrale Satz, deklariert in Theorems/Thm_fermat_last_theorem.lean, besagt, dass für jede natürliche Zahl n größer oder gleich 3 und für jedes Tripel positiver ganzer Zahlen a, b, c gilt: a^n + b^n ≠ c^n. Die Konstruktion umfasst 60.475 Module, alle kompiliert und vom Lean-Kernel während eines Builds von Grund auf überprüft, wie im Repository^[1] berichtet.

Der Mechanismus der doppelten Verifikation

Der Hauptbuild nutzt Lean 4.33.1, eine Version, die die Kernel-Soliditätskorrektionen aus 2026 integriert. Mathlib wird vollständig aus der Quelle neu kompiliert, wodurch jede Abhängigkeit von vorgefertigten Artefakten eliminiert wird, die stille Diskrepanzen einführen könnten. Dies beseitigt das Risiko, Kompilierungsfehler von früheren Versionen der mathematischen Bibliothek zu erben – ein wiederkehrendes Problem in Toolchains, die gepufferte Caches zwischen Projekten wiederverwenden.

Die Datei FinalCheck.lean erzwingt eine präzise Einschränkung: Der Build schlägt fehl, es sei denn, der Beweis stützt sich exakt auf die drei Standardaxiome von Lean, propext, Classical.choice und Quot.sound. Null Instanzen von sorry, null hinzugefügte Axiome, null Verwendung von native_decide.

Eine zweite Kontrollebene kommt vom Komparator leanprover/comparator v4.33.0, der den Build gegen verification/comparator/Challenge.lean abgleicht. Der gemeldete Bescheid, „Your solution is okay!", bestätigt die Identität zwischen der bewiesenen Aussage und der in reinem Mathlib deklarierten Herausforderung.

Der unabhängige Kernel als Vertrauensgrenze

Die dritte Ebene stammt von nanoda 0.4.13, einem in Rust geschriebenen Lean-Kernel, unabhängig von der offiziellen Implementierung. Er akzeptierte den Export der gleichen Umgebung, die vom Hauptbuild erzeugt wurde.

Diese doppelte Überprüfung, offizieller Kernel plus alternativer Kernel, reproduziert exakt die Logik des unabhängigen Validierungskreislaufs, den diese Rubrik für jede Pipeline empfiehlt, bei der die Ausgabe einer Komponente zur Eingabe der nächsten wird. Der Unterschied liegt darin, dass die Domäne hier die formale Mathematik ist, in der semantische Mehrdeutigkeit konstruktionsbedingt abwesend ist.

Die Grundbedingung, die formale Mathematik und Multi-Agent-Systeme verbindet

Die strukturelle Bedingung, die diese Verifikation und unternehmensweite Multi-Agent-Systeme gemeinsam haben, ist dieselbe: Eine kritische Ausgabe muss durch einen unabhängigen Validierungspfad bestätigt werden, bevor sie als zuverlässig betrachtet wird. Der Unterschied ist, dass hier ein formaler Kernel existiert, der diese Bestätigung deterministisch durchführen kann.

In auf Sprachmodelle basierenden Produktionssystemen fehlt dieser deterministische Kernel. Das Fehlen eines formalen Schiedsrichters zwingt Teams, explizite Schutzschalter zu konstruieren, sonst verbreitet sich der Fehler eines Agenten unbremst durch die gesamte Pipeline – exakt der Mechanismus, der in Studien zur Hallucination-Kaskade dokumentiert ist.

Das Risiko, das Modell auf andere Domänen zu übertragen

Das Hauptrisiko betrifft nicht die Korrektheit des Beweises, der durch drei unabhängige Kontrollebenen bestätigt wurde. Es betrifft vielmehr die Versuchung, die Methode auf Domänen zu verallgemeinern, wo vollständige Formalisierung unpraktikabel ist, wie die meisten auf natürlicher Sprache basierenden unternehmensweiten Entscheidungsprozesse.

Die formale Mathematik besitzt eine Eigenschaft, die kein Vertragsdokument oder RAG-Abruf-Pipeline besitzt: Eine beweisbare Aussage hat exakt einen Wahrheitswert, mechanisch überprüfbar. Ein aus einem RAG-System abgerufenes Dokument hingegen trägt intrinsische semantische Mehrdeutigkeit und kann böswillige Anweisungen als legitimer Inhalt verschleiert enthalten. Das Behandeln des einen als Modell des anderen erzeugt einen Beschaffungsfehler: Man kauft formale Verlässlichkeit für Probleme, die probabilistisch bleiben.

Drei Fragen für unternehmensweite AI-Teams

Bevor dieses Ergebnis als wiederverwendbares Präzedenzfall behandelt wird, sollte jedes technische Team drei operative Fragen beantworten:

1. Welcher Teil der unternehmensweiten Pipeline verfügt heute über einen Äquivalent des unabhängigen Kernels, der eine Ausgabe bestätigen kann, bevor sie zur nachgelagerten Eingabe wird?
2. Welche impliziten Axiome, Abhängigkeiten, Versionen, gepinnten Bibliotheken bleiben dokumentiert und welche werden stillschweigend angenommen?
3. Wer im Team hat die Autorität, einen Build oder eine Freigabe zu blockieren, falls die unabhängige Überprüfung ein abweichendes Ergebnis meldet?

Entscheidungen für den nächsten Planungszyklus

CTOs und Chief Digital Officers sollten formale Verifikationsstapel als eigenständige Investitionskategorie neu bewerten, unterschieden vom generischen AI-Tooling. Heads of Engineering sollten die Übernahme von Dual-Kernel-Praktiken oder zumindest Kreuzvalidierung für kritische Pipelines erwägen, wo Fehler hohe Kosten verursachen.

CFOs sollten dieses Ergebnis als Signal lesen, dass die Investition in formale Methoden, historisch als akademisch angesehen, nun überprüfbare Artefakte mit geringen Audit-Kosten produziert. Das Technology Procurement Committee sollte Verträge mit Verifikations-Tooling-Anbietern neu verhandeln und dokumentierte Belege für unabhängige Kontrolle fordert, die der hier beschriebenen entspricht.

Die technischen Grenzen, die nicht übersehen werden dürfen

Das Repository erklärt seinen Status explizit: „Research artifact. Not maintained and not accepting contributions", wie im Repository^[1] berichtet. Dies positioniert das Projekt in eine Kategorie unterschieden von produktionsbereit: verfügbar zur Überprüfung, ausschließlich als Referenzform, ohne Kanal für kontinuierliche Wartung.

Das von Anthropic veröffentlichte Forschungspapier zur Formalisierung rahmt die Übung als Demonstration der Fähigkeiten aktueller Modelle bei Aufgaben des assistierten mathematischen Denkens ein, verfügbar auf anthropic.com^[2]. Die Kluft zwischen „verfügbar zum Lesen" und „bereit für Integration in Produktions-Workflows" bleibt der Punkt, den jeder Beschaffungsausschuss fest im Auge behalten muss, bevor er die Initiative auf unternehmensweite Domänen repliziert, die weniger formalisierbar sind als Zahlentheorie.