Une démonstration qu’une machine peut vérifier
Anthropic a annoncé le 4 septembre qu’un modèle interne de recherche a produit la première démonstration du dernier théorème de Fermat vérifiable de bout en bout par ordinateur. La formalisation représente environ 13 millions de lignes de Lean, l’assistant de preuve que les mathématiciens utilisent pour contraindre chaque étape d’un raisonnement à une forme qu’une machine peut contrôler. Le travail a pris onze jours, selon Anthropic.
Le dernier théorème de Fermat affirme qu’aucun triplet d’entiers positifs ne satisfait a^n + b^n = c^n pour un entier n supérieur à deux. Andrew Wiles l’a démontré en 1995 dans un article d’environ 129 pages, appuyé sur un appareil mathématique construit tout au long du XXe siècle. Relire une telle démonstration à la main prend des années aux spécialistes. On attendait un délai comparable pour la formaliser.
Ce que le modèle a réellement fait
Selon Anthropic, il s’agissait d’un modèle interne polyvalent, à peu près comparable à Claude Fable 5.1, et non d’un moteur mathématique dédié. L’entreprise indique que plusieurs dizaines d’agents ont travaillé en parallèle, produisant environ six milliards de tokens et démontrant 30 300 théorèmes, dont 29 500 figurent dans le résultat final. L’intervention humaine s’est limitée à des orientations générales.
Anthropic précise que les premières tentatives ont échoué. L’exécution qui a abouti reposait sur une plateforme interne appelée Prove2Me, qui suit les dépendances entre théorèmes et permet à de nombreux agents de travailler sur des branches distinctes de la même démonstration sans perdre le fil. Environ sept pour cent des lignes non routinières du fichier final proviennent des tentatives ratées.
Le socle humain sous le résultat
Le résultat ne sort pas de nulle part. Il suit une version simplifiée du raisonnement de Wiles exposée par Henri Darmon, Fred Diamond et Richard Taylor, et s’appuie sur Mathlib, la bibliothèque mathématique communautaire que des milliers de contributeurs construisent en Lean depuis plus de dix ans, ainsi que sur le projet de formalisation dirigé par Kevin Buzzard à l’Imperial College de Londres. Buzzard, qui a relu le résultat, en a résumé la portée en termes de fiabilité : les artefacts, dit-il, sont désormais assez solides pour qu’on bâtisse dessus.
Anthropic a elle-même signalé des limites. La démonstration ne repose que sur les trois axiomes standard de Lean, et un comparateur a confirmé que l’énoncé démontré correspond bien à la formulation du théorème dans Mathlib — le contrôle qui empêche un système de démontrer quelque chose de subtilement plus faible que ce qu’il annonce. Mais l’entreprise reconnaît aussi que la démonstration est probablement bien plus longue que nécessaire, ce qui compte pour qui voudrait en réutiliser les morceaux.
Pourquoi la formalisation est le point intéressant
Les mathématiques connaissent depuis des décennies un goulot d’étranglement dans la vérification : les démonstrations de pointe sont si longues qu’une poignée de personnes seulement peuvent les arbitrer, et des erreurs ont survécu à la publication. La formalisation supprime le problème de l’arbitre, au prix d’une quantité énorme de travail fastidieux. Ce compromis l’a maintenue rare.
Si la moitié fastidieuse peut être automatisée à cette échelle, le calcul change. Cela s’ajoute à une série d’annonces comparables : Anthropic a publié en août des travaux sur de nouveaux résultats obtenus par Claude autour de la fonction zêta de Riemann, et OpenAI affirme que son modèle Astra a résolu plusieurs problèmes d’Erdős restés ouverts.
Ce qu’il faut surveiller, c’est la réutilisation indépendante. Un fichier Lean de 13 millions de lignes est vérifiable par construction — c’est tout l’objet de Lean — mais sa valeur pour les mathématiciens en exercice dépend de la possibilité d’intégrer les théorèmes intermédiaires à Mathlib et de les employer ailleurs. Anthropic n’a pas dit quand, ni si, l’artefact complet serait publié à cette fin.
