Claude formalise la démonstration du théorème de Fermat en Lean

L'entreprise Anthropic a annoncé le 4 septembre 2026 que son intelligence artificielle Claude avait produit la toute première démonstration du dernier théorème de Fermat entièrement vérifiable par ordinateur, du début à la fin. Le théorème énonce qu'il n'existe aucun triplet d'entiers positifs a, b, c tel que a^n + b^n = c^n pour un entier n supérieur à 2. Plus de trente ans après la démonstration de 129 pages publiée par le mathématicien Andrew Wiles en 1995, aucune vérification mécanique intégrale de sa logique n'avait jamais été menée. Claude a travaillé de façon largement autonome pendant 11 jours et a produit environ 13 millions de lignes de code dans le langage de preuve formelle Lean.

Le projet a été mené par Tianyi Peng, chercheur chez Anthropic spécialisé dans la formalisation mathématique par IA. Au fil du travail, Claude a démontré, sous une forme vérifiable par ordinateur, environ 30 300 théorèmes intermédiaires, dont environ 29 500 ont été effectivement utilisés dans la démonstration finale. Le volume de code produit dépasse cinq fois la taille de Mathlib, la principale bibliothèque mathématique communautaire pour Lean. Des dizaines d'agents Claude ont travaillé en parallèle pour définir des concepts et démontrer des théorèmes intermédiaires, avant de s'attaquer à des énoncés de plus en plus difficiles. Les premiers essais ont toutefois échoué : les agents perdaient la trace de l'état global du projet et ne parvenaient plus à réutiliser efficacement leurs résultats respectifs. Environ 7 % des lignes non répétitives de la démonstration finale proviennent de ces tentatives ratées.

Ce qu'est une démonstration formelle vérifiée par ordinateur

Un article de mathématiques destiné à des lecteurs humains omet souvent les étapes jugées « évidentes ». Un assistant de preuve comme Lean, lui, doit voir chaque étape, aussi triviale soit-elle : rien ne peut être laissé implicite. Réécrire une démonstration existante sous cette forme s'appelle la « formalisation ». Si un seul maillon de la chaîne logique casse, tout ce qui en dépend peut s'effondrer — c'est pourquoi une démonstration formalisée n'obtient une garantie de validité indépendante de toute relecture humaine qu'une fois qu'elle a passé le contrôle mécanique de Lean. Celle de Claude ne repose que sur les trois axiomes standards de Lean, sans aucun « sorry » — le marqueur qui permet de laisser temporairement une étape non démontrée. Un outil de comparaison a confirmé que l'énoncé démontré correspond à celui du théorème de Fermat tel qu'il figure dans Mathlib, et un noyau Lean indépendant écrit en Rust, nommé « nanoda », a vérifié plus d'un million de déclarations sans erreur.

Pourquoi Fermat est un cas emblématique

Le théorème de Fermat tire son nom d'une note griffonnée vers 1637 par le mathématicien français Pierre de Fermat dans la marge d'un exemplaire de l'Arithmétique de Diophante, où il affirmait avoir découvert « une démonstration véritablement merveilleuse », que la marge était trop étroite pour contenir. Pendant plus de 350 ans, des générations de mathématiciens ont cherché cette démonstration sans succès. En 1908, un prix équivalent aujourd'hui à un à deux millions de dollars a été promis à qui la trouverait ; 621 tentatives erronées sont arrivées dès la première année. En juin 1993, Andrew Wiles a annoncé sa démonstration lors d'une série de conférences de trois jours, mais un défaut critique a été repéré environ deux mois plus tard, pendant la relecture. Il lui a fallu près d'un an, avec son ancien étudiant Richard Taylor, pour le corriger avant de publier la version définitive en mai 1995 — 129 pages, dont la vérification a demandé des mois de travail à la communauté mathématique. Fait notable pour un lecteur international : la conjecture de Taniyama-Shimura, sur laquelle repose la démonstration de Wiles, a été formulée dans les années 1950 par les mathématiciens japonais Yutaka Taniyama et Goro Shimura. C'est une version simplifiée de la démonstration de Wiles, due à Darmon, Diamond et Taylor, que Claude a formalisée.

Cette extraordinaire réussite d'autoformalisation, qui n'a demandé que 11 jours selon les chercheurs d'Anthropic, démontre le théorème de Fermat sans aucune hypothèse en dehors des axiomes des mathématiques. On y voit au passage l'autoformalisation de l'algèbre, de l'analyse harmonique, de la géométrie et de la théorie des nombres, et on y apprend que les artefacts d'autoformalisation produits par l'IA sont désormais assez solides pour qu'on puisse construire dessus : la démonstration est structurée en plusieurs couches.

• Durée du travail : 11 jours, largement en autonomie
• Code Lean produit : environ 13 millions de lignes, plus de 5 fois Mathlib
• Théorèmes démontrés : environ 30 300, dont 29 500 utilisés dans la démonstration finale
• Jetons de sortie consommés : environ 6 milliards, avec un modèle de recherche comparable à Claude Fable 5.1
• Axiomes utilisés : les 3 axiomes standards de Lean uniquement, zéro « sorry »

Ce que Claude a fait — et ce qu'il n'a pas fait

Un point mérite d'être souligné : Claude n'a pas « découvert » seul la démonstration originale de Wiles. Le raisonnement mathématique a été établi par Wiles et ses collaborateurs en 1995 ; le travail de Claude a consisté à réécrire une version simplifiée de ce raisonnement sous la forme symbolique rigoureuse que Lean peut vérifier, puis à la faire contrôler mécaniquement — c'est la « formalisation », pas la découverte. Cela diffère nettement des travaux récents de l'IA sur l'hypothèse de Riemann, qui visaient à produire de nouvelles mathématiques. Anthropic situe explicitement la nouveauté de ce travail du côté de la vérification, pas de la découverte. Le travail s'est appuyé sur Prove2Me, une plateforme collaborative de formalisation mathématique développée par Tianyi Peng, qui gère les dépendances entre théorèmes sous la forme d'un graphe orienté acyclique afin que plusieurs agents Claude sachent quel théorème attaquer ensuite. L'intervention humaine s'est limitée à des instructions de haut niveau de la part de Peng, comme « prioriser le jacobien en tant que schéma ».

À mesure que l'IA produit davantage de démonstrations mathématiques, la charge de vérification humaine s'alourdit. Anthropic estime que produire une démonstration formalisée et vérifiable par ordinateur, en parallèle d'un article destiné à des lecteurs humains, va devenir une pratique courante. Kevin Buzzard, qui dirige depuis 2024 un projet communautaire pluriannuel de formalisation du théorème de Fermat sous Lean (dont le seul plan de travail initial atteint déjà 86 pages), voit dans cette réussite un pas important vers l'autoformalisation de la littérature mathématique moderne — de quoi débusquer des erreurs dans le corpus existant, alléger la charge des relecteurs, et vérifier rigoureusement des mathématiques produites par des IA.

Pour une entreprise française, l'enseignement dépasse la seule prouesse mathématique. Les mêmes assistants de preuve formelle qui vérifient un théorème peuvent vérifier un protocole cryptographique, un composant critique de système embarqué (aéronautique, ferroviaire, énergie) ou une spécification logicielle — des secteurs où la France dispose déjà d'une expertise reconnue en méthodes formelles, portée notamment par l'Inria et l'outil Coq. L'apport d'agents IA capables de produire des millions de lignes de preuve en quelques jours, là où une équipe humaine mettait des années, ouvre une piste concrète pour accélérer la certification de logiciels critiques — à condition, comme le rappelle Anthropic lui-même, de ne jamais confondre cette capacité de vérification avec une capacité de découverte mathématique autonome.