Claude formalise le dernier théorème de Fermat en 11 jours

Claude a travaillé en grande partie de manière autonome pendant 11 jours et a produit une preuve vérifiée par ordinateur du dernier théorème de Fermat, la formalisation comptant 13 millions de lignes de code Lean et prouvant 29 500 théorèmes intermédiaires, soit plus de cinq fois la taille de Mathlib, la principale bibliothèque de preuves mathématiques. Avec Prove2Me et un harnais multi-agents basé sur Claude Code, une équipe d'agents a achevé la preuve en un peu moins de deux semaines, consommant environ six milliards de jetons de sortie d'un modèle de recherche interne à usage général approximativement comparable à Claude Fable 5.1. La campagne reposait sur Prove2Me, une plateforme collaborative ouverte développée par le chercheur d'Anthropic Tianyi Peng et ses collaborateurs de son groupe à l'Université Columbia, qui maintient un graphe acyclique dirigé d'énoncés de théorèmes que des dizaines d'agents Claude ont utilisé en parallèle pour décider quelles sous-preuves tenter ensuite. Premier énoncé par Pierre de Fermat en 1637, le dernier théorème de Fermat est resté sans preuve jusqu'à ce qu'Andrew Wiles publie sa solution révolutionnaire en 1995. Une tâche dont on estimait qu'elle prendrait des années a été achevée en 11 jours. La preuve complète a été vérifiée de manière indépendante par nanoda, un noyau de preuve séparé écrit en Rust, qui a confirmé que les 1 052 234 déclarations sont correctes. Kevin Buzzard a souligné les implications plus larges : « Si la formalisation automatique du FLT est possible aujourd'hui, alors nous avons fait un grand pas vers la formalisation automatique de la littérature mathématique moderne. De telles techniques d'autoformalisation conduiront à de nouveaux outils, révélant les erreurs du corpus mathématique actuel et allégeant la charge des relecteurs. »