Claude ne résout pas Fermat : il rend sa preuve vérifiable par Lean

Anthropic publie la première formalisation complète du dernier théorème de Fermat, produite en onze jours par plusieurs agents Claude et vérifiée avec l’assistant de preuve Lean.

Le dernier théorème de Fermat n’a pas été résolu une seconde fois par une intelligence artificielle. Sa démonstration était connue depuis les travaux d’Andrew Wiles et Richard Taylor, publiés en 1995. La nouveauté annoncée par Anthropic se trouve ailleurs : Claude a transformé cette démonstration en une chaîne de raisonnement que Lean peut vérifier intégralement, étape après étape.

Cette distinction évite de présenter l’expérience comme une nouvelle découverte mathématique. Claude n’a ni trouvé une preuve inconnue ni reconstitué la mystérieuse démonstration que Pierre de Fermat affirmait avoir découverte au XVIIe siècle. Il a formalisé une voie déjà établie, issue des travaux de Frey, Serre, Ribet, Wiles et Taylor-Wiles.

L’exploit reste considérable. La preuve humaine mobilise plusieurs domaines avancés, de la théorie des nombres à la géométrie algébrique, en passant par les représentations galoisiennes et les formes modulaires. Une équipe de plusieurs dizaines d’agents Claude en a produit une version complète en Lean en onze jours, entre le 7 et le 17 août 2026. Anthropic a publié le résultat le 4 septembre.

L’énoncé tient pourtant en une ligne : pour tout entier naturel (n) supérieur ou égal à 3, il n’existe aucun triplet d’entiers strictement positifs (a), (b) et (c) vérifiant (a^n + b^n = c^n). Cette apparente simplicité a résisté aux mathématiciens pendant plus de trois siècles.

Vers 1637, Fermat avait noté dans la marge d’un exemplaire de l’Arithmetica de Diophante qu’il possédait une démonstration « véritablement merveilleuse », mais que l’espace disponible était trop étroit pour la contenir. Aucun texte correspondant n’a été retrouvé. Les techniques nécessaires à la preuve moderne n’existaient pas à son époque, ce qui conduit généralement les historiens des mathématiques à penser que son raisonnement comportait une erreur ou ne couvrait qu’un cas particulier.

Andrew Wiles annonça une première démonstration en 1993. Une vérification menée par plusieurs spécialistes révéla ensuite une faille importante. Wiles travailla pendant environ un an à la corriger, d’abord seul puis avec Richard Taylor. Les deux articles établissant la preuve complète furent finalement publiés en 1995.

Cette histoire illustre la difficulté de vérifier un raisonnement mathématique complexe. Même lorsqu’un texte est rédigé par un chercheur reconnu et relu par des spécialistes, une étape apparemment secondaire peut fragiliser tout ce qui en dépend. Les démonstrations destinées aux humains omettent aussi de nombreux passages considérés comme évidents, renvoient à des résultats antérieurs ou utilisent des conventions communes à une discipline.

Un assistant de preuve comme Lean ne partage pas cette connaissance implicite. Chaque définition doit être formulée précisément, chaque hypothèse rendue visible et chaque transition justifiée à partir d’éléments déjà admis ou démontrés. Lean contrôle ensuite que le nouveau résultat découle bien de ces fondations.

La formalisation ne consiste donc pas à copier un article dans un autre format. Elle oblige à reconstruire l’architecture logique de la preuve, à combler ses raccourcis et à représenter dans un langage rigoureux les objets mathématiques qu’elle emploie. Une démonstration lisible en quelques dizaines ou centaines de pages peut ainsi devenir un dépôt informatique immense.

Claude a produit environ 13 millions de lignes de Lean, dont près de 10,5 millions hors éléments générés automatiquement. La formalisation contient 29 511 théorèmes dans la chaîne dont dépend le résultat final, auxquels s’ajoutent environ 533 000 lemmes locaux intégrés aux fichiers. Près de 30 300 théorèmes avaient été démontrés sur la plateforme à la fin du projet, mais tous n’ont pas été conservés dans le chemin final.

Anthropic souligne que le dépôt dépasse cinq fois la taille de Mathlib, la principale bibliothèque mathématique utilisée par Lean. La comparaison donne une idée du volume, mais ne mesure pas directement la complexité. Mathlib est une bibliothèque condensée, réutilisable et relue par sa communauté, tandis que la production de Claude reste très redondante et probablement beaucoup plus longue que nécessaire.

Le dépôt publié sur GitHub le présente d’ailleurs comme un artefact de recherche qui ne sera pas maintenu et n’accepte pas de contributions. Anthropic reconnaît que son contenu n’est pas encore dans un état qui permettrait son intégration directe à Mathlib.

La preuve ne part pas non plus d’une page blanche. Elle repose sur Mathlib et reprend des éléments provenant de deux projets ouverts : la formalisation communautaire dirigée par Kevin Buzzard à l’Imperial College de Londres et le projet `flt-regular`, consacré aux nombres premiers réguliers. Le document technique recense 106 fichiers adaptés de ces travaux avec attribution.

Ce socle est important pour comprendre l’autonomie revendiquée. Les agents ont écrit l’essentiel des nouvelles déclarations et démonstrations, mais ils disposaient déjà d’une bibliothèque formelle, de travaux humains antérieurs et d’une présentation mathématique détaillée de la voie à suivre. L’expérience mesure leur capacité à développer et relier ces fondations, pas leur aptitude à réinventer seuls plusieurs siècles de théorie des nombres.

La formalisation suit principalement une présentation publiée en 1995 par Henri Darmon, Fred Diamond et Richard Taylor. Elle reprend une version simplifiée du raisonnement de Wiles et Taylor-Wiles plutôt que la voie plus récente choisie par le projet de Kevin Buzzard.

Dans ses grandes lignes, le raisonnement suppose qu’un contre-exemple au théorème existe, puis lui associe une courbe elliptique particulière, appelée courbe de Frey. Cette courbe devrait posséder des propriétés incompatibles : les travaux de Wiles conduisent à la considérer comme modulaire, tandis que le théorème d’abaissement du niveau de Ribet entraîne une situation impossible. La contradiction élimine le contre-exemple supposé.

Formaliser cette structure exige bien