Fermat formalisé en 28,7 heures par 1 000 agents Claude : ce que l'expérience d'Anthropic démontre vraiment

Ce qu'il faut retenir

L'expérience d'Anthropic ne démontre rien de nouveau sur le dernier théorème de Fermat, qui est prouvé depuis 1995. Elle montre autre chose : une équipe de 1 000 agents d'IA, coordonnés seulement par un dépôt Git et une base de données, a su réécrire en un peu plus d'une journée une preuve que l'ordinateur vérifie de bout en bout. Le résultat est réel dans son principe, mais il a été obtenu avec beaucoup plus d'aide que ne le dit l'annonce, sur une seule exécution, et sans vérification extérieure publiée à ce jour.

Le chiffre mis en avant vient du billet de lancement de Claude Fable 5.2, le 9 novembre 2026 : 1 000 agents auraient « entièrement formalisé le théorème en 30 heures seulement, avec une intervention humaine minimale » (traduction Le Latent). Le détail se trouve dans un second texte, publié le même jour sur le blog technique claude.dev par cinq membres d'Anthropic, qui parle d'une « expérience jouet » et d'une durée de 28,7 heures. Notre article sur le lancement de Fable 5.2 et ses prix couvre le reste de l'annonce.

Formaliser une preuve, ce n'est pas la trouver

Pierre de Fermat a énoncé vers 1637 qu'aucun entier positif ne vérifie aⁿ + bⁿ = cⁿ pour n supérieur à 2. Andrew Wiles l'a démontré en 1995 dans une preuve de 129 pages, rappelle Anthropic. Formaliser cette preuve consiste à la réécrire dans Lean, un assistant de preuve : chaque étape, même évidente pour un humain, doit être écrite, et le noyau du logiciel l'accepte ou la refuse. Si tout passe et que l'énoncé final est bien le bon, la preuve est correcte, sous les axiomes de Lean.

Ce chantier était un objectif ancien de la communauté. Depuis 2024, le mathématicien Kevin Buzzard (Imperial College London) dirige un projet collectif pour formaliser une version moderne de la preuve, décrit sur le site de Lean, qui y voit le dernier théorème restant de la liste des 100 défis de formalisation de Freek Wiedijk.

Le 4 septembre 2026, Anthropic a pris de l'avance : un modèle interne, comparable selon l'entreprise à Claude Fable 5.1, a produit en 11 jours une preuve complète de 13 millions de lignes de Lean, avec environ 6 milliards de tokens de sortie, la plateforme Prove2Me de l'université Columbia et les consignes ponctuelles d'un chercheur. C'est ce travail que l'expérience de novembre reproduit.

Ce que les agents avaient réellement en main

Le billet de lancement affirme que Fable 5.2 n'a utilisé « aucune référence mathématique, seulement une liste d'énoncés intermédiaires pour mesurer ses progrès ». Le billet technique donne une liste plus longue : 60 énoncés à prouver (le théorème final et 59 jalons), une esquisse d'une phrase de la démarche classique, les définitions utilisées par ces énoncés, 47 lemmes déjà prouvés tirés de la formalisation de septembre, et Mathlib, la bibliothèque de mathématiques de Lean. Numerama a relevé le même écart le 10 novembre 2026.

Le tableau ci-dessous rassemble les deux versions et la formalisation de septembre.

Source : Anthropic, billet de lancement, billet claude.dev et billet de recherche du 4 septembre 2026, relevés le 10 novembre 2026.

Ces 47 lemmes et ces 60 jalons découpent déjà le chemin : l'équipe savait par où passer. Le gain revendiqué porte donc sur l'organisation et la vitesse d'exécution, pas sur la découverte de la route.

Comment 1 000 agents se sont organisés

C'est la partie la plus instructive pour qui construit des agents d'IA. Selon le billet technique, chaque agent tournait dans sa propre machine virtuelle, sans accès au réseau, avec un shell, un éditeur, Lean et sa branche Git. Un agent chef dirigeait 999 aides. Dans les 10 premières minutes, il a créé cinq tables dans une base Postgres partagée (ordres, affectations, notes, sous-tâches, travail terminé), puis réparti les énoncés entre des équipes de 16 ou 17 aides.

Les agents se sont trompés sur la difficulté. Au départ, les aides ont jugé 47 énoncés sur 60 infaisables dans le temps imparti ; les 10 énoncés jugés faisables ont été prouvés en 70 minutes environ, et le chef a relancé l'équipe sur les autres. Le dernier obstacle, le théorème de Langlands–Tunnell, a mobilisé environ 750 aides et un arbre de 2 418 tâches sur 10 niveaux, alors que son capitaine lui donnait moins de 1 % de chances d'aboutir. Il est tombé à 28,4 heures, le théorème final à 28,7 heures, d'après Anthropic.

Trois détails techniques comptent pour un ingénieur. Sur une seule machine partagée, le système plafonnait vers 100 agents : plus de la moitié de ces essais ont dû être arrêtés ou relancés faute de mémoire, de disque ou de processeur. Le dispositif a envoyé au chef 19 rappels automatiques du temps restant, chacun l'encourageant à continuer. Et un classifieur a examiné plus d'un million d'appels d'outils sans en bloquer aucun, selon le même billet. Les auteurs concluent eux-mêmes que les agents abandonnent trop tôt les problèmes durs et qu'un encouragement humain reste utile.

Ce qui n'a pas été vérifié de l'extérieur

La preuve de septembre a été contrôlée par la personne la mieux placée pour le faire. Kevin Buzzard écrit l'avoir compilée et passée au comparateur, qui vérifie que l'énoncé prouvé est bien celui de Fermat : « it checks out ». Il mesure 13,4 millions de lignes, dont la compilation prend près de 20 fois plus de temps que celle de Mathlib sur une machine à 96 cœurs. En réponse à un lecteur, il précise avoir inspecté la centaine de lignes qui n'étaient ni une définition ni une preuve. Anthropic indique de son côté que la preuve n'utilise que les trois axiomes standard de Lean.

Rien de comparable n'est annoncé pour la preuve de novembre. Le billet technique cite le correcteur automatique de l'expérience et un message du chef d'équipe, « Fermat's Last Theorem is on main, kernel-checked by the official checker ». Mais aucun des deux textes du 9 novembre 2026 ne renvoie vers un dépôt public de cette nouvelle preuve ni ne mentionne de relecture extérieure, au moment où nous les avons lus, le 10 novembre 2026. Le dépôt public de la preuve de septembre, lui, n'a pas reçu de modification depuis le 24 septembre 2026, d'après son historique GitHub consulté le même jour. La figure finale du billet technique s'arrête d'ailleurs à 54 énoncés sur 60 : cinq variantes sont devenues inutiles et un énoncé a été abandonné en route.

La comparaison avec Claude Opus 5.5, qui n'aurait bouclé que 26 % du travail en 18 heures avec le même dispositif, repose sur une seule exécution par modèle, précise la légende du graphique d'Anthropic. C'est un indice, pas une mesure répétée.

Ce que ça change, et ce que ça coûte

Sur le plan mathématique, rien. Kevin Buzzard l'a écrit dès septembre : ce travail « ne nous apprend essentiellement rien » (traduction Le Latent), puisqu'il suit fidèlement la littérature de 1995. Son propre projet continue, avec d'autres buts : enrichir Mathlib et produire un document lisible par des humains, selon son billet. Ce qui change, c'est la faisabilité de la vérification automatique de mathématiques de haut niveau, que Buzzard juge prometteuse pour la relecture des articles. C'est la même logique que pour les réfutations de l'hypothèse du temps exponentiel vérifiées en Lean : une preuve formelle garantit l'énoncé qu'elle prouve, pas le récit qui l'accompagne.

Anthropic ne donne aucun coût. Un ordre de grandeur se calcule à partir de ses chiffres : la formalisation de septembre a consommé environ 6 milliards de tokens de sortie, celle de novembre un tiers, soit environ 2 milliards. Au prix catalogue de Fable 5.2, 40 dollars par million de tokens de sortie, cela représente de l'ordre de 80 000 dollars, sans compter les tokens d'entrée. C'est une illustration : l'expérience a tourné en interne sur une version préliminaire, et le coût réel pour Anthropic n'est pas connu.

Pour un lecteur qui doit juger l'annonce, la bonne lecture tient en une phrase : Lean rend une preuve vérifiable, mais une affirmation sur une preuve ne l'est que si la preuve est publiée et contrôlée. En septembre, elle l'a été ; en novembre, pas encore. D'autres travaux d'Anthropic sur la vérification, comme FlashProve et ses preuves d'inférence, appellent la même prudence. Google DeepMind a appliqué la même méthode, agents et Lean, au code de chiffrement de Signal le 10 novembre 2026 : voir ce que prouve AlphaProof Code, et ce qu'il suppose. Les autres analyses de résultats publiés sont dans les Comparatifs du Labo.