Anthropic a publié le 4 septembre la première formalisation complète et vérifiée par ordinateur de la preuve du théorème de Fermat, produite par Claude en onze jours, de façon largement autonome. Le résultat : 13 millions de lignes de Lean, 30 300 théorèmes intermédiaires démontrés dont 29 500 utilisés dans la preuve finale, un dépôt public sous licence Apache 2.0 avec trois chemins de vérification. Kevin Buzzard (Imperial College London), qui mène depuis 2024 le projet humain de formalisation du même théorème avec une subvention d'un million de livres sur cinq ans, a compilé le code, lancé l'outil de comparaison, et confirmé : la preuve tient, avec pour seules hypothèses les trois axiomes standard de Lean.
- Ce n'est pas une nouvelle preuve : Claude a traduit en code vérifiable la preuve de Wiles et Taylor, en suivant l'exposé de Darmon, Diamond et Taylor de 1995, un chemin différent de celui, plus moderne, que Buzzard formalisait
- L'artefact fait plus de cinq fois la taille de Mathlib, la bibliothèque communautaire sur laquelle tout projet Lean s'appuie ; le calcul a consommé environ 6 milliards de tokens de sortie, soit de l'ordre de 300 000 dollars au tarif public du modèle, un tiers de la subvention de Buzzard dépensé en onze jours
- La première tentative a échoué : les agents perdaient la trace des résultats déjà démontrés et dupliquaient le travail ; c'est l'ajout de Prove2Me, une plateforme open source de Columbia qui organise la preuve en graphe de dépendances, qui a rendu la fin possible
Ce qui a été fait, ce qui ne l'a pas été, et ce qui a rendu la chose possible
Formaliser une preuve, c'est la réécrire dans un langage qu'un assistant de preuve vérifie ligne à ligne, sans ambiguïté ni confiance à accorder à l'auteur. La preuve de Wiles fait environ 130 pages en prose mathématique dense et s'appuie sur des décennies de résultats ; chacun devait être formalisé à son tour. C'est pourquoi le projet de Buzzard, lancé en 2024, était budgété sur cinq ans. Claude n'a pas découvert de mathématiques nouvelles : il a converti une route connue en 13 millions de lignes que Lean accepte. Buzzard le dit lui-même : sur les mathématiques, ça ne change rien ; sur la formalisation, c'est un grand pas vers la formalisation automatique de la littérature mathématique moderne.
La partie la plus instructive du rapport d'Anthropic est l'échec initial. Les premières exécutions multi-agents se sont effondrées : chaque agent accumulait trop de contexte local, perdait de vue les lemmes déjà prouvés et refaisait le travail des autres. Ce qui a débloqué la situation, c'est Prove2Me, un outil open source de l'équipe de Tianyi Peng (Columbia, aussi chercheur chez Anthropic) qui maintient un graphe orienté de tous les énoncés à prouver, marque ceux qui le sont, et distribue les objectifs. Les agents ne coordonnaient plus entre eux ; ils coordonnaient via une structure de données que le vérificateur alimente. La direction humaine s'est limitée à quelques indications de haut niveau de Peng.
Cette recette a un nom générique : générer beaucoup, vérifier mécaniquement, garder ce qui passe. C'est celle qu'OpenAI a appliquée un mois plus tôt avec Astra sur dix problèmes ouverts, pour 2 000 dollars. Ici, l'échelle est cent fois supérieure et le coût est à l'avenant ; ce que les deux cas partagent, c'est que le modèle n'a jamais été cru sur parole. Le point d'attribution que soulève la couverture spécialisée est légitime : Mathlib, le projet FLT de Buzzard et Prove2Me sont des infrastructures communautaires sans lesquelles rien n'aurait tourné, et Anthropic les cite, mais le titre retient « Claude ».
Mon avis : la nouvelle n'est pas que l'IA « résout Fermat », c'est qu'un chantier de cinq ans devient un job de onze jours dès qu'un vérificateur existe. Le coût, encore prohibitif pour un laboratoire universitaire, baissera ; la méthode, elle, est déjà reproductible partout où l'on sait écrire un test. C'est la capacité que Fable 5.1 a doublée sur Terminal-Bench-Science, mise en scène sur le théorème le plus célèbre du monde.
Ce que ça change pour vous
Si vous êtes loin des mathématiques, la leçon est la même que pour Astra, en plus net : les tâches qui ont un vérificateur (tests, schémas, règles, compilateur) sont celles où des agents en boucle rendent aujourd'hui des résultats hors de portée d'une équipe. Les autres, non. Et le détail des agents qui « perdaient la trace » est directement transposable : un essaim d'agents sans état partagé et vérifié se marche dessus ; un graphe de tâches maintenu par le vérificateur, pas par les agents, est ce qui tient.
- Pour tout flux multi-agents, sors l'état d'avancement des agents : une liste de tâches avec statut vérifié mécaniquement (test passé, fichier validé), que chaque agent lit avant d'agir, à la manière du graphe de Prove2Me
- Avant de lancer une boucle générer-vérifier à grande échelle, calcule le coût en tokens de sortie par succès sur un échantillon : ici, c'est 300 000 dollars pour un succès, la rentabilité dépend entièrement de ce que vaut le résultat
- Si tu communiques sur un résultat obtenu avec des agents, nomme les infrastructures tierces qui l'ont permis : c'est la critique la plus fréquente faite à Anthropic cette semaine, et elle est fondée
Sources
- Anthropic - Formalizing Fermat's Last Theorem (4 septembre 2026)
- The Next Web - Claude formalised Fermat's Last Theorem in 11 days (réaction de Kevin Buzzard, chemin de preuve suivi)
- Yahoo News - calcul du coût en tokens et comparaison avec la subvention EPSRC
- AI Weekly - échec de la première tentative, rôle de Prove2Me, question de l'attribution
Source : Anthropic.com
Cet article a été rédigé avec l’assistance d’un modèle de langage (LLM).
