L’intelligence artificielle d’Anthropic formalise le dernier théorème de Fermat en seulement onze jours
Il a fallu près de 360 ans aux mathématiciens pour démontrer cette conjecture, faite par le mathématicien Pierre de Fermat en 1637. Mais vérifier la fiabilité d’une démonstration peut aussi prendre énormément de temps, et c’est là que l’IA est intervenue.
le 09/09/2026 13:30
Temps de lecture : 2min
La start-up américaine Anthropic a annoncé que son programme Claude avait réalisé la « première démonstration complète et vérifiée par ordinateur du dernier théorème de Fermat », dans un communiqué publié le 4 septembre.
Le dernier théorème de Fermat, conjecturé par Pierre de Fermat en 1637, est « l’une des conjectures mathématiques les plus célèbres de tous les temps ». Cette conjecture stipule qu’« aucun entier positif a, b, c ne satisfait à l’équation aⁿ + bⁿ = cⁿ pour tout n > 2. » La première démonstration, réalisée par Sir Andrew Wiles en 1995, comptait 129 pages et a nécessité des mois de travail minutieux pour être vérifiée.
« Comprendre un résultat novateur suffisamment en profondeur pour être sûr de son exactitude peut prendre des mois, voire des années, de travail. »
Anthropicdans un communiqué
Pour faciliter la vérification, des tentatives ont été faites pour « formaliser » la démonstration dans une forme lisible par un ordinateur. Selon Anthropic, Claude a produit, en 11 jours et de manière autonome, la première démonstration de bout en bout du dernier théorème de Fermat, vérifiée par ordinateur. Ce processus a nécessité l’écriture de 13 millions de lignes de code Lean et la démonstration de 29 500 théorèmes intermédiaires.
Des équipes d’agents de Claude ont collaboré pour définir des concepts et démontrer des théorèmes intermédiaires, mais plusieurs tentatives initiales ont échoué. Grâce à une collaboration avec la plateforme Prove2Me, ils ont réussi à mener à bien la démonstration en un peu moins de deux semaines, consommant environ six milliards de tokens de sortie.
Kevin Buzzard, mathématicien à l’Imperial College de Londres, a salué cette avancée comme une « extraordinaire prouesse », affirmant que ces techniques d’auto-formalisation pourraient mener à de nouveaux outils pour réduire les erreurs dans le corpus mathématique et alléger la charge de travail des évaluateurs.
Source : Franceinfo
