Anthropic : Claude réalise une démonstration vérifiée par ordinateur du dernier théorème de Fermat

Selon l'entreprise, c'est "une avancée majeure vers un avenir où l’ensemble des mathématiques pourra être facilement vérifié". La startup américaine Anthropic, en pointe en matière d'intelligence artificielle (IA), 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é vendredi 4 septembre.

Le dernier théorème de Fermat, conjecturé par le mathématicien français Pierre de Fermat en 1637, est "l’une des conjectures mathématiques les plus célèbres de tous les temps", explique Anthropic, qui la résume ainsi : "Aucun entier positif a, b, c ne satisfait à l’équation aⁿ + bⁿ = cⁿ pour tout n > 2." Il a fallu plus de trois siècles pour obtenir la première démonstration de ce théorème, réalisée par Sir Andrew Wiles en 1995 ; elle "comptait 129 pages et a nécessité des mois de travail minutieux pour être vérifiée", raconte la startup.

"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."

Pour accélérer ce long processus de vérification, certains ont tenté de "formaliser" la démonstration, en la réalisant dans une forme lisible par un ordinateur (notamment grâce à l’assistant Lean). C'est sur cette étape que Claude a impressionné, selon Anthropic : "En 11 jours, en travaillant de manière largement autonome, Claude a produit la première démonstration de bout en bout du dernier théorème de Fermat, vérifiée par ordinateur. Au cours de ce processus, il a écrit 13 millions de lignes de code Lean et démontré 29 500 théorèmes intermédiaires."

Une "extraordinaire prouesse"

"Des dizaines d’agents de Claude ont collaboré pour définir des concepts, démontrer des théorèmes intermédiaires et utiliser ces derniers pour prouver des énoncés de plus en plus complexes", raconte l'entreprise. Plusieurs des premières tentatives ont "échoué", car les agents "ont rapidement perdu de vue l’état d’avancement du projet et ont cessé de collaborer efficacement". Mais grâce à une collaboration avec la plateforme Prove2Me, des agents IA "ont mené à bien la démonstration en un peu moins de deux semaines, en consommant environ six milliards de tokens de sortie provenant d'un modèle d'IA à usage général dédié à la recherche en interne, à peu près comparable à Claude Fable 5.1".

Kevin Buzzard, mathématicien à l’Imperial College de Londres qui mène depuis 2024 un effort collectif pour formaliser cette démonstration, a salué une "extraordinaire prouesse". "De telles techniques d’auto-formalisation déboucheront sur de nouveaux outils, permettant d’éradiquer les erreurs dans le corpus mathématique actuel et d’alléger la charge de travail des évaluateurs", explique le spécialiste. L'automatisation évitera également d'être noyé sous la vérification des résultats générés par les IA, "ce qui constitue actuellement un processus mené par des humains extrêmement coûteux", ajoute Kevin Buzzard.