Une démonstration qu’il a fallu sept ans à un mathématicien pour concevoir, et un projet de cinq ans à un autre chercheur pour formaliser, vient d’être achevée par une équipe d’agents d’IA en onze jours. Le modèle Claude d’Anthropic a produit une version formelle du dernier théorème de Fermat, l’un des problèmes les plus célèbres de l’histoire des mathématiques. Il ne s’agit pas d’une nouvelle démonstration. C’est quelque chose d’on ne peut plus utile : une confirmation lisible et vérifiée par machine indiquant que la démonstration humaine est correcte, construite à partir de zéro dans un langage de programmation appelé Lean.
Un problème vieux de 350 ans, et ce que signifie réellement la « formalisation »
Le dernier théorème de Fermat énonce qu’aucun nombre entier a, b et c ne peut satisfaire l’équation aⁿ + bⁿ = cⁿ lorsque n est un nombre entier supérieur à 2. Pierre de Fermat a posé cette énigme au XVIIe siècle, notant de sa main dans la marge d’un manuel qu’il avait trouvé une démonstration, mais qu’il manquait d’espace pour l’écrire. Cette note a hanté les mathématiques pendant environ trois siècles et demi.
Andrew Wiles a finalement démontré le théorème en 1995, après avoir travaillé sur le problème en secret pendant sept ans. Sa démonstration n’a pas été sans difficulté : une faille a été découverte, et il a fallu environ un an à Wiles et à son collaborateur Richard Taylor pour la corriger. Cet épisode illustre une vulnérabilité structurelle des démonstrations mathématiques traditionnelles. Elles sont écrites en langage naturel et en notation logique, vérifiées par des experts humains, et vulnérables à des erreurs qui peuvent se cacher au sein de longues chaînes de raisonnement.
La formalisation s’attaque directement à cette vulnérabilité. Elle consiste à traduire une démonstration en code informatique, plus précisément dans un langage formel qu’une machine peut vérifier étape par étape. Il n’y a aucune ambigüité dans le code. Soit la logique tient, soit elle ne tient pas. Un dépôt central appelé Mathlib stocke déjà environ 2 millions de lignes de mathématiques formalisées. La nouvelle démonstration d’Anthropic ajoute 13 millions de lignes à ce paysage, couvrant environ 29 500 théorèmes intermédiaires nécessaires pour atteindre le résultat final. Cela représente plus de cinq fois la taille de tout le contenu précédent de Mathlib combiné, et la plus grande démonstration en Lean jamais écrite.
Comment les agents ont réellement fonctionné (et où ils ont eu des difficultés)
Le système d’Anthropic n’a pas utilisé un seul modèle d’IA travaillant de manière isolée. De nombreux agents distincts ont été déployés, chacun se voyant assigner différentes portions du problème, s’attaquant à des fragments plus petits du théorème en parallèle. Le processus a fonctionné de manière continue et autonome pendant onze jours.
Les experts humains n’étaient pas absents. Ils ont fourni ce qu’Anthropic décrit comme des « instructions de haut niveau » pour garder le travail sur la bonne voie. Il convient de le noter : les agents ont périodiquement perdu le fil de l’état global du projet et ont cessé de collaborer efficacement. Le système a nécessité une orientation externe pour se remettre de ces pannes. Ce qui a finalement aidé, c’est un outil conçu à l’origine pour la collaboration mathématique humaine, appelé Prove2Me. Une fois que les agents ont commencé à l’utiliser pour suivre leur travail et se coordonner sur les prochaines étapes, le projet a progressé de manière plus fiable.
Kevin Buzzard, mathématicien à l’Imperial College de Londres qui dirigeait un projet de cinq ans visant à formaliser la même démonstration de Wiles et Taylor, a commenté le résultat. Il a souligné que la démonstration ne repose sur « aucune autre hypothèse que les axiomes des mathématiques », et a décrit le travail comme multicouche, touchant à l’algèbre, à l’analyse harmonique, à la géométrie et à la théorie des nombres. Son évaluation est importante : Buzzard n’était pas un simple spectateur. Il avait organisé une conférence à Londres au début de cette année rassemblant des experts en IA, des informaticiens et des mathématiciens pour travailler précisément sur ce problème. L’annonce d’Anthropic a complètement éclipsé cet effort.
Pourquoi cela compte au-delà du théorème lui-même
Voici ce que la plupart des couvertures médiatiques de cette histoire oublient. Le théorème en soi n’est pas le point central. Le dernier théorème de Fermat était déjà démontré. Ce qu’Anthropic a démontré concerne la nature de la connaissance mathématique et la manière dont elle peut être vérifiée, étendue et consolidée.
Buzzard l’a exprimé directement : si l’IA peut désormais auto-formaliser une démonstration de cette complexité, alors la formalisation automatique de la littérature mathématique moderne dans son ensemble devient un objectif réaliste à court terme. C’est un changement important. Les mathématiques sont le fondement de la physique, de la cryptographie, de l’informatique et de l’ingénierie. Un ensemble de connaissances mathématiques formalisé et vérifiable par machine permettrait aux chercheurs de s’appuyer sur des résultats antérieurs avec bien plus de confiance, en détectant des erreurs que la revision humaine pourrait manquer et en accélérant le rythme auquel de nouveaux résultats peuvent être établis.
L’épisode illustre également un aspect important de la façon dont les systèmes d’IA opèrent actuellement dans le cadre de travaux intellectuels à fort enjeu. Ils ne sont pas autonomes de la manière dont le mot est parfois employé sans rigueur. Ils ont nécessité une supervision humaine, ont connu des pannes de coordination et ont eu besoin d’outils conçus pour la collaboration humaine pour fonctionner efficacement. Le calendrier de onze jours est remarquable. Le besoin d’une orientation humaine tout au long du processus est tout aussi instructif.
Ici, l’IA ne remplace pas les mathématiciens. Elle gère un volume et une granularité de vérification logique qu’aucun equipo humain ne pourrait soutenir à cette échelle, libérant les chercheurs pour qu’ils se concentrent sur les questions de plus haut niveau concernant ce qu’il faut démontrer et pourquoi cela importe.
En bref
Les agents d’IA d’Anthropic ont produit la plus grande démonstration formelle jamais écrite, vérifiant le dernier théorème de Fermat en code Lean lisible par machine à travers 13 millions de lignes et 29 500 étapes intermédiaires. Le résultat importe moins en tant que découverte mathématique qu’en tant que démonstration que l’IA peut désormais formaliser des démonstrations complexes et multicouches à une échelle et à une vitesse auparavant hors de portée. Le processus a nécessité une orientation humaine et a connu des pannes à plus d’une reprise. Ce contexte fait également partie de l’histoire.
D’après un reportage de New Scientist.