Le 4 septembre, Anthropic a annoncé que son modèle Claude avait produit en onze jours une preuve du dernier théorème de Fermat entièrement vérifiable par ordinateur. La formule mérite d'être décortiquée. Claude n'a pas redémontré le théorème. Andrew Wiles l'a fait en 1994, après trois siècles et demi de tentatives ratées. L'IA a traduit cette démonstration déjà admise dans un langage que la machine peut contrôler étape par étape, une opération que les mathématiciens appellent « formaliser ».

Ce que veut dire « formaliser »

Le théorème de Fermat énonce qu'aucun triplet d'entiers positifs a, b, c ne vérifie aⁿ + bⁿ = cⁿ dès que n dépasse 2. Pierre de Fermat l'a griffonné en marge d'un ouvrage en 1637, en assurant en détenir la preuve. Il a fallu attendre 1994 et Andrew Wiles, appuyé par Richard Taylor, pour en venir à bout, rappelle franceinfo. La démonstration publiée en 1995 tient sur 129 pages. Wiles est passé par un détour, en établissant un cas du théorème de modularité qui relie courbes elliptiques et formes modulaires, résultat dont l'énoncé de Fermat se déduit.

Une preuve écrite pour des humains saute les étapes jugées évidentes. Un assistant de preuve comme Lean, ou son cousin Rocq (l'ancien Coq), n'en tolère aucune. Formaliser une démonstration, c'est la réécrire dans un langage si strict qu'un logiciel peut valider chaque micro-inférence, depuis les axiomes de départ jusqu'à la conclusion. Anthropic le note dans son billet, ce qui est nouveau ici tient à la vérification, non aux mathématiques. L'entreprise compare l'exercice au fait de refaire un calcul avec une calculatrice pour s'assurer qu'il est juste. Une fois cette réécriture acceptée par le logiciel, la démonstration ne repose plus que sur une poignée d'axiomes de base et sur l'absence de bug dans le noyau de Lean, ce qui met une preuve à l'abri des erreurs que la relecture humaine laisse parfois passer.

Onze jours, treize millions de lignes

Le modèle employé n'est pas le plus puissant du catalogue d'Anthropic. L'entreprise parle d'un modèle de recherche interne « comparable à Claude Fable 5.1 », lancé sur le problème avec deux phrases de consignes seulement. En onze jours de travail largement autonome, il a généré environ 13,4 millions de lignes de code Lean et démontré 30 300 théorèmes intermédiaires, dont 29 500 servent à la preuve finale, détaille Anthropic. Le tout a consommé près de 6 milliards de tokens, pour un coût estimé autour de 300 000 dollars selon The Next Web. Des équipes de mathématiciens estimaient qu'une formalisation manuelle de la preuve de Wiles réclamerait plusieurs années de travail. Le propre chantier de Kevin Buzzard, financé sur cinq ans, visait ce même objectif.

Les premières tentatives ont échoué. Livrés à eux-mêmes, les agents « perdaient rapidement le fil de l'état d'avancement » et cessaient de coopérer. Le déblocage est venu d'une plateforme de coordination baptisée Prove2Me, qui maintient un graphe des dépendances entre théorèmes et laisse plusieurs instances de Claude travailler en parallèle. Mêmes modèles, mêmes poids, un échec puis un succès, avec cet échafaudage pour seule variable ajoutée. Le projet était piloté par Tianyi Peng, de l'université Columbia. La formalisation suit l'approche dite de Darmon-Diamond-Taylor et couvre les exposants supérieurs ou égaux à 17, les cas plus petits ayant déjà été traités par des travaux antérieurs.

« Ça tient », confirme Kevin Buzzard

C'est un humain qui a validé le résultat. Kevin Buzzard, mathématicien à l'Imperial College de Londres, mène depuis 2024 un projet communautaire de formalisation du même théorème, financé à hauteur d'un million de livres sur cinq ans. Il raconte sur son blog avoir d'abord pris le courriel d'Anthropic pour celui d'un « farfelu ». Puis il a compilé le code, lancé l'outil de comparaison censé vérifier que l'énoncé formalisé correspond bien au vrai théorème, et inspecté à la main chaque ligne que Claude ne présentait pas comme une définition ou une preuve mathématique. Verdict : « ça tient », avec pour seules hypothèses les trois axiomes standard de Lean. Il salue une « prouesse extraordinaire », rapporte franceinfo. C'était la dernière entrée non cochée de la fameuse liste des 100 défis de formalisation de Freek Wiedijk.

Ce que ça ne prouve pas

Buzzard tient à doucher un malentendu. Sur le plan mathématique, dit-il, ce travail « n'apporte essentiellement rien », car la formalisation suit fidèlement la littérature existante et n'y ajoute aucune idée neuve. Il s'agit de vérifier une démonstration déjà acceptée, pas d'en trouver une. La distinction sépare cet épisode d'autres percées récentes de l'IA en mathématiques, où Claude avait produit de nouveaux résultats, comme le contre-exemple qui a fait tomber la conjecture jacobienne en juillet. Sur ce qu'un tel exploit signifie vraiment, le débat n'est pas neuf.

Le résultat garde d'ailleurs les traces de sa méthode brute. La preuve pèse environ cinq fois plus que Mathlib, la bibliothèque mathématique de référence de Lean, et se compile près de vingt fois plus lentement sur une machine à 96 cœurs, note The Next Web. Elle ne peut pas rejoindre Mathlib pour l'instant, la bibliothèque refusant les contributions relues par une IA. Et elle ne part pas de rien, puisqu'elle s'appuie sur la fraction des mathématiques déjà formalisée par des humains.

Un signal pour l'autoformalisation

Ce que l'épisode démontre, selon Buzzard, tient au champ de l'autoformalisation. Si des milliers de pages de littérature peuvent être formalisées de bout en bout par un essaim d'agents en onze jours, la vérification automatique de recherches récentes « au fil de l'eau » devient envisageable. Le mathématicien avance auprès de franceinfo que ces techniques déboucheront sur des outils capables de traquer les erreurs du corpus mathématique et d'alléger un travail de vérification aujourd'hui « extrêmement coûteux ». Il se dit intéressé par la perspective de passer des programmes entiers, comme celui de Langlands, à la moulinette d'une machine qui signale sans complaisance les arguments incomplets.

Deux limites subsistent. La preuve n'a fait l'objet d'aucune relecture humaine de son contenu mathématique, au-delà des vérifications logicielles et de l'inspection par Buzzard des lignes non mathématiques. Et tant que Mathlib refuse les contributions relues par une IA, ces 13,4 millions de lignes demeureront hors de la bibliothèque de référence de Lean.