Anthropic hat den ersten vollständig computergeprüften formalen Beweis des Großen Fermatschen Satzes (FLT) vorgelegt, der von autonomen Claude-Agenten innerhalb von 11 Tagen in der Sprache Lean generiert wurde. Das Projekt umfasst 13 Millionen Zeilen Lean-Code sowie 29.500 bewiesene Zwischensätze und stützt sich auf die mathematische Formulierung von Darmon, Diamond und Taylor (1995). Ermöglicht wurde die Skalierung durch die kollaborative Plattform Prove2Me, die Beweisabhängigkeiten über gerichtete azyklische Graphen (DAGs) parallelisiert und verwaltet, bei einem Rechenaufwand von ca. sechs Milliarden Output-Tokens.
Wichtigste Punkte
Autonome Formalisierung in Rekordzeit: Claude erstellte innerhalb von 11 Tagen einen lückenlosen, maschinell verifizierten Beweis von FLT mit 13 Millionen Zeilen Lean-Code und 29.500 Zwischensätzen. Der Umfang übersteigt den der mathematischen Kernbibliothek Mathlib um das Fünffache.
Beweispfad und Axiomatik: Der Beweis folgt der vereinfachten Wiles-Darstellung von Darmon, Diamond und Taylor. Die Prüfung erfolgte strikt innerhalb des Lean-Beweisassistenten und stützt sich ausschließlich auf dessen drei Standardaxiome; die semantische Äquivalenz der Behauptung wurde über den Lean-Komparator gegen Mathlib validiert.
Strukturierung über Prove2Me: Die Koordination der Agenten erfolgte über die Open-Source-Plattform Prove2Me (Columbia University). Diese zerlegt den Beweis in einen gerichteten azyklischen Graphen (DAG), trennt Theoreme von Beweisen zur Reduktion von Lean-Kompilierzeiten und verhindert Kontextverluste der KI-Modelle.
Ressourcen und Infrastruktur: Für die Formalisierung wurden ca. sechs Milliarden Output-Tokens eines internen Forschungsmodells (äquivalent zu Claude Fable 5.1) aufgewendet. Die Validierung des Gesamtrepositories erforderte 300 GB RAM und 96 CPU-Kerne.
Skalierbarkeit auf Standardhardware: In einem Begleitversuch formalisierten drei persönliche Claude-Max-Instanzen über Prove2Me die Hardy-Littlewood-Kreismethode und Vinogradovs Dreiprimzahlensatz innerhalb von drei Tagen.
Transformation des Peer-Review-Prozesses: Die automatisierte Verifikation soll die manuelle, oft jahrelange Validierung mathematischer Arbeiten fundamental verkürzen und das Entdecken latenter logischer Fehler im mathematischen Korpus beschleunigen.
Diskussions-Highlights
Verifikationssicherheit und Kernel-Integrität: Diskutiert wird, warum 13 Millionen Zeilen Code vertrauenswürdig sind. Nach dem Curry-Howard-Isomorphismus skaliert die Fehlerwahrscheinlichkeit nicht mit der Länge des Beweises, sondern hängt allein von der Korrektheit des minimalen Lean-Typenprüfers ab. Dennoch verweisen Teilnehmer auf frühere Kernel-Schwachstellen (z. B. ein fehlerhafter Collatz-Beweis) und fordern redundante Verifikationen in Systemen wie Metamath oder HOL-Light.
Mathematische Tiefe und Methodik: Kevin Buzzards Begleitpublikation stellt klar, dass Anthropic Fontaine-Theorie und Mazurs Arbeiten zum Eisenstein-Ideal formalisierte, um Punkte der Ordnung $p \ge 17$ auf Frey-Kurven auszuschließen. Dies schließt nahtlos an bestehende Formalisierungen für reguläre Primzahlen an.
Wiederverwendbarkeit vs. Code-Qualität: Mehrere Kommentatoren bezweifeln den didaktischen und strukturellen Nutzen der 13 Millionen Zeilen für Mathlib. Während das Ziel menschlicher Formalisierung modular wiederverwendbare Abstraktionen sind, liefere KI-generierter Code primär monolithischen, schwer lesbaren Beweis-Spaghetti-Code.
Ökonomischer Vergleich: Die geschätzten API-Tokenkosten von ca. 300.000 US-Dollar ($50 pro Million Tokens) werden Kevin Buzzards 5-jährigem, mit 1 Million GBP dotiertem EPSRC-Forschungsprojekt gegenübergestellt.
Relevanz für die Softwaretechnik: Softwareingenieure betonen, dass der drastische Kosten- und Zeitabfall bei formalen Methoden deren Einsatz in der industriellen Softwareverifikation und Systemarchitektur unmittelbar wirtschaftlich macht.
Referenzierte Ressourcen und Tools: Genannt werden Kevin Buzzards Blogpost ("FLT: Anthropic has beaten me to it"), Simon Singhs Dokumentationsband, Freek Wiedijks Liste der 100 formalisierten Theoreme sowie Open-Source-Verifikationswerkzeuge wie open-atp (arXiv:2608.25220) und Warrant.
Glossar
Großer Fermatscher Satz (Fermat’s Last Theorem, FLT): Mathematischer Satz, der besagt, dass die Gleichung $a^n + b^n = c^n$ für ganzzahlige Potenzen $n > 2$ keine ganzzahligen positiven Lösungen für $a, b, c$ besitzt.
Lean: Eine funktionale Programmiersprache und ein interaktiver Beweisassistent, der auf der abhängigen Typentheorie basiert und zur formalen Verifikation mathematischer Beweise und Software verwendet wird.
Mathlib: Die zentrale, von der mathematischen Community gepflegte Open-Source-Bibliothek für formalisierte Mathematik in Lean.
Autoformalisierung: Das automatische Übersetzen von in natürlicher Sprache verfassten mathematischen Beweisen in maschinenprüfbaren Formalcode durch Algorithmen bzw. Sprachmodelle.
Beweisassistent (Proof Assistant): Eine Softwareumgebung, die formalisierte logische Schlussfolgerungen Schritt für Schritt auf mathematische Korrektheit und Konsistenz mit definierten Axiomen überprüft.
Propositions-as-Types (Curry-Howard-Isomorphismus): Ein Grundprinzip der theoretischen Informatik, bei dem eine mathematische Aussage als Datentyp und ihr Beweis als Programm bzw. Term modelliert wird, der diesen Typ erzeugt.
DAG (Directed Acyclic Graph / Gerichteter azyklischer Graph): Eine Netzwerkstruktur aus gerichteten Kanten ohne geschlossene Schleifen, die Abhängigkeiten zwischen Theoremen abbildet, sodass Beweisschritte parallelisiert werden können.
Prove2Me: Eine Open-Source-Kollaborationsplattform zur Modularisierung, Verteilung und Koordination groß angelegter mathematischer Formalisierungsaufgaben über Multi-Agenten-Systeme.
Frey-Kurve: Eine spezifische elliptische Kurve, die hypothetischen Lösungen der Fermat-Gleichung zugeordnet wird; der Nachweis, dass solche Kurven nicht modular sein können, war der Schlüssel zu Wiles' Beweis.
Eisenstein-Ideal: Eine algebraische Struktur in der Zahlentheorie (entwickelt von Barry Mazur), die zur Untersuchung von Torsionspunkten auf modularen Kurven und Darstellungen von Galois-Gruppen dient.
Vinogradovs Dreiprimzahlensatz (Vinogradov's Theorem): Ein Satz der analytischen Zahlentheorie, der besagt, dass jede hinreichend große ungerade Zahl als Summe dreier Primzahlen dargestellt werden kann.
Hardy-Littlewood-Kreismethode: Eine analytische Methode zur Abschätzung von Lösungen ganzzahliger Gleichungen (häufig in additiven Primzahlproblemen) mittels komplexer Fourier- und harmonischer Analyse.
Kernel: Der winzige, hochoptimierte Kern eines Beweisassistenten, der für die letztendliche Verifikation der Typkorrektheit zuständig ist und dessen Fehlerfreiheit das gesamte Vertrauensfundament bildet.