Le dernier théorème de Fermat formalisé par des agents IA en onze jours

En onze jours seulement, des agents IA fondés sur le modèle Claude d'Anthropic ont produit la première démonstration entièrement vérifiée par ordinateur du dernier théorème de Fermat — un résultat que la communauté mathématique estimait devoir prendre plusieurs années à accomplir.

Formulé en 1637 par le mathématicien français Pierre de Fermat, ce célèbre théorème affirme qu'il n'existe aucun triplet d'entiers positifs a, b, c vérifiant l'équation an + bn = cn pour un exposant entier n supérieur à 2. Fermat nota dans la marge d'un livre qu'il possédait une « démonstration merveilleuse », mais que la marge était trop étroite pour la contenir. Pendant plus de 350 ans, des générations de mathématiciens cherchèrent en vain cette preuve. C'est finalement le mathématicien britannique Andrew Wiles qui en publia la première démonstration correcte en 1995, après avoir corrigé une faille critique identifiée lors de la vérification — correction réalisée avec son ancien étudiant Richard Taylor. Cette preuve de 129 pages repose sur des outils mathématiques modernes très éloignés de ce que Fermat pouvait connaître.

La nouveauté de l'exploit d'Anthropic ne réside pas dans la découverte d'une nouvelle démonstration, mais dans sa formalisation : il s'agit de traduire la preuve de Wiles en un langage informatique, Lean, que la machine peut vérifier pas à pas, comme une calculatrice vérifie un calcul. Cette opération, connue sous le nom d'autoformalization, est particulièrement ardue : là où un mathématicien peut sauter des étapes jugées évidentes, Lean exige que chaque étape soit explicitement justifiée, et ne peut s'appuyer que sur les portions de mathématiques déjà formalisées. Kevin Buzzard, professeur à l'Imperial College London, avait lancé dès 2024 un effort collaboratif pour mener à bien cette formalisation, dont le seul plan directeur de la première phase couvre 86 pages.

Le projet a été conduit par Tianyi Peng, chercheur chez Anthropic et professeur assistant à l'Université Columbia, en s'appuyant sur la plateforme ouverte Prove2Me qu'il a co-développée. Des dizaines d'agents Claude ont collaboré en parallèle, définissant des concepts, démontrant des théorèmes intermédiaires et assemblant progressivement la preuve complète. Au total, ils ont produit 13 millions de lignes de code Lean — plus de cinq fois la taille de Mathlib, la principale bibliothèque communautaire de preuves formalisées — et établi quelque 29 500 théorèmes intermédiaires, en consommant environ 6 milliards de tokens. Les interventions humaines se sont limitées à quelques orientations de haut niveau, du type « avancer le théorème de Mazur en priorité ».

Les premières tentatives se soldèrent par des échecs : les agents perdaient rapidement le fil du projet et cessaient de coordonner efficacement leurs efforts. L'utilisation de Prove2Me a permis de résoudre ces difficultés de coordination. Buzzard a salué le résultat comme un accomplissement extraordinaire, relevant que la preuve ne repose que sur trois axiomes fondamentaux et couvre simultanément l'algèbre, la géométrie, l'analyse harmonique et la théorie des nombres.

Au-delà du symbole, Anthropic souligne l'enjeu pratique : à mesure que l'IA produit des preuves mathématiques à un rythme croissant, la formalisation automatique permettrait de vérifier mécaniquement leur validité, sans surcharger des experts humains. La preuve complète a été mise en accès libre sur GitHub.