Le 5 septembre 2026, Anthropic a annoncé que Claude avait produit la première preuve entièrement formalisée et vérifiée par machine du théorème de Fermat, dans l’assistant de preuve Lean 4. L’artefact final dépasse les 13 millions de lignes de code Lean — la plus grande preuve jamais écrite dans un proof assistant, plus de cinq fois la taille de Mathlib. Un chantier que les experts estimaient à plusieurs années, bouclé en 11 jours par un essaim d’agents largement autonomes.

Ce qui s’est passé

Rappel : énoncé par Fermat en 1637 — xⁿ + yⁿ = zⁿ n’a pas de solution entière positive pour n > 2 — le théorème n’a été démontré qu’en 1995 par Andrew Wiles, 358 ans plus tard. Ce qui change n’est pas la mathématique : un ordinateur peut désormais en vérifier chaque étape, et la démonstration a été écrite par une IA.

Entre le 7 et le 17 août 2026, une petite équipe d’Anthropic a lancé un run sur Prove2Me, une plateforme conçue par Tianyi Peng et ses collaborateurs de Columbia University : plusieurs dizaines d’agents Claude en parallèle, coordonnés autour d’un graphe de dépendances — le théorème prouvé par un agent devenant une dépendance consommable par les autres. Les humains n’ont écrit ni mathématiques ni code Lean, seulement l’énoncé du théorème final, sur une ligne. Bilan : 29 511 théorèmes dans l’arbre final (30 300 prouvés au total), ≈ 6 milliards de tokens générés, une preuve reposant uniquement sur les trois axiomes standards de Lean, sans aucun sorry.

La vérification ne s’arrête pas au kernel Lean : la preuve a été rejouée sur deux vérificateurs indépendants — nanoda, kernel écrit en Rust, et le comparator de Mathlib — plus d’un million de déclarations contrôlées, zéro erreur. La démonstration suit l’argument de Wiles et Taylor-Wiles — cas particuliers de Mazur, Langlands-Tunnell et Ribet prouvés au passage — et s’appuie sur l’infrastructure open source existante : Mathlib, le projet FLT de l’Imperial College London, flt-regular. Le tout est publié sur GitHub sous licence Apache 2.0.

Pourquoi c’est important

Une nuance d’abord, que les gros titres vont écraser : Claude n’a pas « résolu » Fermat, Wiles l’avait fait en 1995. Claude a formalisé la preuve : traduit un raisonnement de niveau recherche en un artefact que la machine accepte ou rejette, sans zone grise.

Ensuite, l’effet d’entraînement. Kevin Buzzard, qui a relu la preuve, résume : « Si la formalisation automatique de Fermat est possible maintenant, alors nous avons fait un grand pas vers la formalisation automatique de la littérature mathématique moderne. » Anthropic insiste moins sur le trophée que sur les 29 000 théorèmes annexes, prouvés dans des domaines jamais formalisés.

Implications pour les devs et le web

  1. La preuve formelle devient un livrable réaliste. Lean est un langage de programmation : cette preuve est un code que le compilateur accepte ou rejette. Pour les smart contracts, protocoles et systèmes critiques, « ça se prouve » pourrait succéder au « ça compile ».
  2. Une leçon d’architecture d’agents. Le pattern Prove2Me — graphe partagé de dépendances, agents parallèles publiant des résultats vérifiés — est un monorepo avec CI distribuée : la meilleure démo à ce jour d’orchestration d’agents.
  3. Génération massive ≠ confiance aveugle. 13 millions de lignes générées n’ont de valeur que parce qu’un kernel indépendant les valide. Même leçon pour nos codebases : la vérification automatique est ce qui rend la génération de code par IA exploitable.
  4. L’open source est le socle. Mathlib, le projet de l’Imperial College, flt-regular : la prouesse repose sur des centaines de contributeurs et des années de travail communautaire.

Source