Les deux versions sont alignées bloc par bloc, dans l’ordre du texte : titre, l’essentiel, puis paragraphe par paragraphe. Quand la traduction a fusionné ou scindé un paragraphe, la case correspondante reste vide — on ne rapproche jamais deux passages au jugé.
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.
Le moment décisif de ce projet consacré à Fermat est peu spectaculaire : dans Lean, une démonstration se compile — ou ne se compile pas. Le dépôt GitHub d'Anthropic contient désormais, selon l'entreprise, une version entièrement vérifiée par ordinateur du dernier théorème de Fermat. Le mathématicien Kevin Buzzard a depuis compilé lui-même le code et exécuté le comparateur associé.
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.
Sur le plan mathématique, le théorème n'est pas nouveau. Andrew Wiles a démontré en 1995, en 129 pages, que l'équation xⁿ + yⁿ = zⁿ ne possède aucune solution entière pour les exposants entiers n > 2. La nouveauté réside dans la formalisation : la démonstration est traduite en code de façon à ce qu'un ordinateur puisse contrôler chaque étape, plutôt que de s'appuyer sur des étapes intermédiaires omises parce qu'elles semblent évidentes aux humains.
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 est à la fois un langage de programmation et un système de vérification. Les énoncés mathématiques et leurs démonstrations sont vérifiés au regard d'un ensemble fixe de règles logiques ; la moindre lacune empêche la compilation de la démonstration. La confiance doit alors porter avant tout sur le petit noyau de Lean et ses axiomes. La bibliothèque disponible Mathlib limite toutefois le champ aux pans des mathématiques qui ont déjà été formalisés.
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.
Selon Anthropic, des dizaines d'agents Claude ont travaillé pendant onze jours sur une version simplifiée de la démonstration de Wiles, d'après Darmon, Diamond et Taylor. Ils ont produit 13 millions de lignes de code Lean et environ 29 500 théorèmes intermédiaires. Selon l'entreprise, les premières équipes ont échoué à garder une vue d'ensemble du projet ; le travail n'a progressé qu'avec Prove2Me, une plateforme développée par l'équipe de Tianyi Peng à Columbia University, qui gère les étapes suivantes de la démonstration dans un graphe orienté acyclique. Selon Anthropic, l'effort a représenté environ six milliards de tokens de sortie ; on peut en déduire un coût compris entre 100 000 et 300 000 dollars américains.
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.
Concrètement, cela change dès maintenant quelque chose pour la formalisation de la littérature mathématique : des tiers peuvent compiler le code rendu public et vérifier la chaîne logique. Cela offre un contrôle techniquement reproductible, mais ne remplace pas une évaluation indépendante, qui fait encore largement défaut. Buzzard considère cette formalisation comme une avancée majeure vers la formalisation automatique des mathématiques modernes ; elle s'inscrit toutefois dans le prolongement des travaux antérieurs et n'apporte aucun nouvel énoncé mathématique sur le dernier théorème de Fermat.