Anthropic fait vérifier par ordinateur une preuve de Fermat vieille de 30 ans
D'après Anthropic - Formalizing Fermat's Last Theorem et Imperial College London - projet FLT (Kevin Buzzard)
Image : générée (Gemini)
Rédigé à partir de la source originale; chaque fait est vérifié contre le texte source.
À retenir
- Le théorème dit qu'aucun entier positif ne vérifie aⁿ+bⁿ=cⁿ pour n>2. Pierre de Fermat l'a énoncé vers 1637 ; Andrew Wiles en a publié la première preuve complète en 1995, après des mois de vérification humaine.
- « Formaliser » une preuve, c'est la réécrire dans un langage comme Lean pour qu'un ordinateur en vérifie chaque étape logique. La communauté mathématique jugeait ce travail si long qu'elle prévoyait des années pour Fermat.
- Des agents Claude ont travaillé « largement de façon autonome » pendant 11 jours, écrit 13 millions de lignes de Lean et prouvé 29 500 théorèmes intermédiaires utilisés dans la preuve finale, avec la plateforme Prove2Me.
- Le mathématicien Kevin Buzzard (Imperial College London), qui dirige depuis 2024 un projet distinct de formalisation de ce théorème, a relu le résultat et confirme qu'il établit Fermat sans autre hypothèse que les axiomes de Lean.
- Anthropic précise que le travail a consommé environ six milliards de jetons de sortie d'un modèle de recherche interne « comparable à Claude Fable 5.1 » - donc pas nécessairement ce modèle commercial lui-même.
Pourquoi ça compte
Une preuve mathématique acceptée peut rester des années sous vérification humaine avant d'inspirer pleinement confiance - Wiles lui-même a mis des mois à corriger un trou trouvé après coup. Une formalisation informatique élimine ce doute pour la partie qu'elle couvre : si Lean l'accepte, la chaîne logique est correcte. Le geste montre qu'il devient possible de vérifier de grandes preuves déjà connues plus vite qu'avant - pas d'en produire de nouvelles.
Chiffre-clé
13 millions de lignes de code Lean - plus de 5 fois la taille de Mathlib, la bibliothèque communautaire de preuves sur laquelle ce travail s'appuie - écrites en 11 jours, selon Anthropic (4 septembre 2026).
Citation
« This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics. » Kevin Buzzard, mathématicien (Imperial College London), cité par Anthropic
Action concrète
Devant ce genre d'annonce, vérifier si le mot employé est « formaliser » (vérifier une preuve déjà acceptée) ou « démontrer »/« prouver » (établir un résultat mathématique inédit) - ce travail relève du premier cas, pas du second.
Fondée sur la source originale
Sources
- Anthropic - Formalizing Fermat's Last Theorem : Billet de recherche original, publié le 4 septembre 2026.
- Imperial College London - projet FLT (Kevin Buzzard) : Projet distinct de formalisation de Fermat, en cours depuis avril 2024 ; contexte sur le rôle de Kevin Buzzard, retrouvé par recherche indépendante.
🔧 Outils mentionnés