Anthropic : le dernier théorème de Fermat formalisé dans Lean

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é.

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 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.

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.

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.