Le 4 septembre 2026, Anthropic a fait une annonce retentissante dans le monde académique : une flotte d’agents d’IA a achevé la formalisation et la vérification intégrale par machine du dernier théorème de Fermat en seulement 11 jours. En regard, une équipe de mathématiciens de premier plan de l’Imperial College London disposait d’un budget d’un million de livres sterling et avait planifié cinq années pleines pour accomplir cette même tâche.
Cette énigme mathématique, qui a tenu l’humanité en échec pendant plus de 350 ans, a déjà été résolue en 1995 par le Britannique Andrew Wiles. L’enjeu de cette confrontation spectaculaire entre 11 jours et cinq ans ne réside donc pas dans un élargissement des frontières mathématiques en soi.
Ce qu’elle vient véritablement bousculer, c’est le modèle séculaire de confiance intellectuelle fondé sur l’autorité des experts humains. L’examen d’une démonstration majeure est passé d’un « processus d’évaluation par les pairs étalé sur plusieurs années et sujet à l’erreur » à « une validation des ruptures logiques par une machine en quelques minutes ».
Une énigme de 350 ans qui met à nu les failles de la relecture humaine
L’histoire de la résolution du dernier théorème de Fermat ressemble à une longue suite de défaillances des systèmes d’évaluation humaine. En 1908, le prix Wolfskehl dota en Allemagne la démonstration d’une récompense de 100 000 marks-or. Stimulé par cette prime, le comité reçut 621 propositions dès la première année — toutes, sans exception, contenaient des erreurs fatales.
Le cerveau humain présente des angles morts naturels lorsqu’il traite des chaînes logiques d’une immense complexité. En juin 1993, Wiles donna trois conférences à l’Institut Isaac Newton de Cambridge pour annoncer au monde sa démonstration. Pourtant, deux mois plus tard, une question pointue posée par les rapporteurs lors d’une vérification de routine mit en évidence une faille critique au cœur de l’édifice mathématique.
Il fallut à Wiles une année entière d’efforts acharnés, frôlant parfois le renoncement, pour corriger ce point d’achoppement, avant de publier en mai 1995 son article définitif de 129 pages. Réunir quelques grands esprits dans un bureau pour scruter manuellement une centaine de pages de manuscrit touffu poussait déjà les capacités cognitives humaines à leurs limites physiques.
Image : Bannière de l’annonce officielle d’Anthropic. Source : Anthropic
13 millions de lignes de code machine en 11 jours
Comment amener un ordinateur à vérifier un entrelacs d’abstractions mathématiques ? La réponse tient dans la « formalisation » : traduire une démonstration rédigée en prose littéraire, truffée de raccourcis intuitifs, en un code exécutable où pas un signe de ponctuation ni une contrainte de type ne sont tolérés en défaut. Par le passé, cette besogne relevait du travail de bénédictin réservé à une poignée de pionniers.
Le professeur Kevin Buzzard, de l’Imperial College London, pilotait un projet communautaire échelonné sur cinq ans pour formaliser le théorème. Son équipe avait déjà rédigé un « schéma directeur » de 86 pages rien que pour tracer la feuille de route de cette traduction.
Claude, le modèle de recherche d’Anthropic, exécuté sur la plateforme Prove2Me, a réduit cette perspective pluriannuelle à moins de deux semaines. En s’appuyant sur l’argumentaire simplifié de 1995, il a produit plus de 13 millions de lignes de code — un volume représentant plus de cinq fois l’ensemble de la bibliothèque mathématique officielle de la plateforme.
Ce code renferme la preuve formelle de 30 300 lemmes et théorèmes, dont 29 500 ont été intégrés au graphe final. Des dizaines d’agents d’IA ont coopéré en parallèle comme des rouages infatigables, décomposant l’intuition humaine en maillons logiques exécutables ligne à ligne par la machine.
300 000 dollars pour s’offrir une certitude absolue
L’arrivée d’une puissance de calcul industrielle a transformé des coûts humains exorbitants en un bilan comptable direct. Le plan sur cinq ans de l’équipe de Buzzard engageait un million de livres, tributaire des salaires, du temps de réflexion et des échanges continus entre scientifiques.
En regard, la campagne de formalisation menée par Claude a consommé environ 6 milliards de tokens de sortie. Aux tarifs actuels des API publiques, la note s’élève à quelque 300 000 dollars. Obtenir pour 300 000 dollars de calcul la certitude absolue qui exigeait auparavant cinq années de travail humain recompose irréversiblement l’économie de la recherche de pointe.
Les agents n’ont pas progressé sans faux pas. Lors des premières passes, des défaillances de coordination ont entraîné des pertes d’état du projet. Cependant, le système s’est rapidement réajusté par approximations successives : les tentatives avortées représentent environ 7 % des lignes non génériques du code final. Les chercheurs d’Anthropic se sont bornés à fournir des orientations de haut niveau, confiant l’élimination des anomalies aux agents eux-mêmes.
Image : Graphe DAG sur Prove2Me montrant comment Claude décompose les sous-théorèmes pour atteindre FLT. Source : Anthropic
Le mécanisme de confiance scientifique confié au compilateur
Le professeur Kevin Buzzard a personnellement vérifié ce vaste ensemble de plus de dix millions de lignes : le compilateur a validé le code sans la moindre erreur. Des outils de comparaison automatisés ont également confirmé la conformité parfaite de tous les énoncés avec les bibliothèques mathématiques formelles de référence. Cette réussite marque l’achèvement définitif de la liste des « 100 défis de formalisation », ouverte il y a vingt ans.
Comme l’a souligné Buzzard lui-même, aucune découverte mathématique fondamentale n’a été faite, mais l’événement apporte une démonstration éclatante de la viabilité de la formalisation automatisée. Lorsqu’une démonstration de 129 pages peut être compilée à l’instar d’un logiciel informatique, les rouages de la confiance académique se trouvent profondément modifiés.
Jadis, l’approbation d’un théorème reposait sur le cautionnement moral de quelques figures tutélaires. Ce modèle d’autorité centralisée est désormais remis en cause. Dès lors qu’un code traverse le compilateur avec succès, la vérité n’a plus besoin d’aval humain. Le compilateur assure désormais le rôle de juge de paix.
Liens de référence :
- Anthropic Research
- Discussion HN
