Both versions are aligned block by block, in reading order: title, the essentials, then paragraph by paragraph. Where the translation merged or split a paragraph, the matching cell stays empty — we never pair two passages by guesswork.
Der entscheidende Moment dieses Fermat-Projekts ist unspektakulär: In Lean kompiliert ein Beweis – oder er tut es nicht. Im GitHub-Repository von Anthropic liegt nach Angaben des Unternehmens nun eine vollständig computergeprüfte Fassung von Fermats letztem Satz. Der Mathematiker Kevin Buzzard hat den Code inzwischen selbst kompiliert und den zugehörigen Komparator ausgeführt.
The decisive moment in this Fermat project is unspectacular: in Lean, a proof either compiles or it does not. Anthropic’s GitHub repository now contains what the company describes as a fully computer-checked version of Fermat’s Last Theorem. Mathematician Kevin Buzzard has since compiled the code himself and run the associated comparator.
Mathematisch ist der Satz nicht neu. Andrew Wiles bewies 1995 auf 129 Seiten, dass die Gleichung xⁿ + yⁿ = zⁿ für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen hat. Neu ist die Formalisierung: Der Beweis wird so in Code übersetzt, dass ein Computer jeden einzelnen Schritt kontrollieren kann, statt sich auf übersprungene, für Menschen offensichtliche Zwischenschritte zu verlassen.
Mathematically, the theorem is not new. Andrew Wiles proved in 1995, over 129 pages, that the equation xⁿ + yⁿ = zⁿ has no integer solutions for integer exponents n > 2. What is new is the formalization: the proof is translated into code so that a computer can check every single step, rather than relying on intermediate steps that have been skipped because they are obvious to humans.
Lean ist dabei Programmiersprache und Prüfsystem zugleich. Mathematische Aussagen und ihre Herleitungen werden gegen ein festes logisches Regelwerk geprüft; wenn auch nur eine Lücke bleibt, kompiliert der Beweis nicht. Vertrauen muss dann vor allem dem kleinen Kern von Lean und seinen Axiomen gelten. Die verfügbare Bibliothek Mathlib begrenzt den Spielraum allerdings auf den Teil der Mathematik, der bereits formalisiert wurde.
Lean serves as both a programming language and a verification system. Mathematical statements and their derivations are checked against a fixed set of logical rules; if even one gap remains, the proof will not compile. Trust must then rest primarily on Lean’s small core and its axioms. The available Mathlib library does, however, limit the scope to the areas of mathematics that have already been formalized.
Anthropic zufolge arbeiteten Dutzende Claude-Agenten elf Tage lang an einer vereinfachten Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Heraus kamen 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Erste Teams scheiterten laut dem Unternehmen am Projektüberblick; vorangekommen sei die Arbeit erst mit Prove2Me, einer von Tianyi Pengs Gruppe an der Columbia University entwickelten Plattform, die nächste Beweisschritte in einem gerichteten azyklischen Graphen verwaltet. Der Aufwand lag laut Anthropic bei rund sechs Milliarden Output-Token; daraus lassen sich Kosten zwischen 100.000 und 300.000 US-Dollar hochrechnen.
According to Anthropic, dozens of Claude agents worked for eleven days on a simplified version of Wiles’ proof following Darmon, Diamond and Taylor. The result was 13 million lines of Lean code and around 29,500 intermediate theorems. According to the company, the first teams failed to maintain an overview of the project; the work only made progress with Prove2Me, a platform developed by Tianyi Peng’s group at Columbia University that manages the next proof steps in a directed acyclic graph. According to Anthropic, the effort amounted to around six billion output tokens; that translates into estimated costs of between $100,000 and $300,000.
Konkret ändert sich damit schon jetzt etwas für die Formalisierung mathematischer Literatur: Dritte können den offengelegten Code kompilieren und die logische Kette prüfen. Das schafft eine technisch reproduzierbare Kontrolle, ersetzt aber keine unabhängige Bewertung, die bislang weitgehend aussteht. Buzzard hält die Formalisierung für einen großen Schritt hin zur automatischen Formalisierung moderner Mathematik; zugleich folgt sie der frühen Literatur und liefert keine neue mathematische Aussage über Fermats letzten Satz.
This is already changing something concrete about the formalization of mathematical literature: third parties can compile the disclosed code and check the logical chain. That creates a technically reproducible form of verification, but it does not replace an independent assessment, which is still largely pending. Buzzard considers the formalization a major step toward the automated formalization of modern mathematics; at the same time, it follows the early literature and offers no new mathematical statement about Fermat’s Last Theorem.