Claude formalise Fermat en 11 jours : ce que ça dit des agents IA

06/09/2026

Le 4 septembre 2026, Anthropic a annoncé que des dizaines d’agents Claude ont produit en 11 jours, presque sans intervention humaine, la première preuve du théorème de Fermat vérifiée par ordinateur dans le langage Lean : 13 millions de lignes, 29 500 théorèmes intermédiaires, 6 milliards de tokens

Anthropic a annoncé le 4 septembre 2026 que des dizaines d’agents Claude ont produit en 11 jours, presque sans intervention humaine, la première preuve complète du théorème de Fermat vérifiée par ordinateur dans le langage Lean : 13 millions de lignes de code, 29 500 théorèmes intermédiaires, environ 6 milliards de tokens. Le mathématicien Kevin Buzzard, qui menait le même projet depuis 2024 sur plusieurs années, a recompilé le résultat et le confirme. Ce n’est pas une découverte mathématique. C’est la démonstration la plus nette à ce jour de ce qu’une équipe d’agents abat seule sur une tâche longue, à condition qu’une machine vérifie chaque étape.

Ce qu’Anthropic a annoncé

Le théorème de Fermat, énoncé en 1637 et démontré par Andrew Wiles en 1995 dans une preuve de 129 pages, restait le dernier de la liste des cent défis de formalisation dressée par Freek Wiedijk il y a vingt ans. Le formaliser, c’est la réécrire dans un langage que l’ordinateur vérifie ligne à ligne. Dans son billet de recherche, Anthropic détaille l’opération :

11 jours de travail, la racine de la preuve passant à l’état « prouvé » le 18 août 2026 à 2 h du matin, heure UTC.
13 millions de lignes de Lean, soit cinq fois la taille de Mathlib, la bibliothèque mathématique de référence du langage. Anthropic reconnaît que sa preuve est « probablement beaucoup plus longue qu’elle ne devrait l’être ».
30 300 théorèmes intermédiaires démontrés, dont 29 500 servent dans la preuve finale, sans aucune hypothèse ajoutée aux trois axiomes standards de Lean.
Environ 6 milliards de tokens en sortie, produits par un modèle de recherche interne qu’Anthropic décrit comme « à peu près comparable à Claude Fable 5.1 ».

Infographie : la formalisation du théorème de Fermat par Claude en quatre chiffres : 11 jours de travail autonome, 13 millions de lignes de Lean soit cinq fois Mathlib, 29 500 théorèmes intermédiaires utilisés dans la preuve finale, environ 6 milliards de tokens en sortie — Un volume qu’aucune équipe humaine ne produit en onze jours, et que seul un vérificateur automatique peut relire.

Comment des dizaines d’agents ont travaillé sans chef

La première tentative d’Anthropic a échoué : les agents perdaient de vue l’état du projet, accumulaient trop de contexte local et refaisaient le travail des autres. Le succès est venu de Prove2Me, une plateforme ouverte conçue par Tianyi Peng et son équipe à l’université Columbia. Elle découpe la preuve en un graphe d’énoncés dépendants et décrit chaque théorème en langage courant pour que les agents le retrouvent et le réutilisent. Autour, un harnais bâti sur Claude Code fait tourner des dizaines d’agents en parallèle. L’apport humain s’est limité à quelques consignes de haut niveau, du genre « pousse le théorème de Mazur ». Même les échecs ont servi : environ 7 % des lignes utiles de la preuve finale viennent de tentatives abandonnées.

Schéma : à gauche, l’exposé de 1995 de la preuve de Wiles, la bibliothèque Mathlib et quelques consignes humaines occasionnelles ; au centre, des dizaines d’agents Claude coordonnés par Prove2Me pendant 11 jours ; à droite, Lean qui accepte ou rejette chaque étape, une preuve complète de 13 millions de lignes, et la relecture indépendante de Kevin Buzzard — Le juge n’est pas l’humain ni le modèle : c’est le compilateur Lean, qui accepte ou rejette chaque étape sans discussion.

Ce que ça ne prouve pas

Kevin Buzzard, professeur à l’Imperial College de Londres, a passé le résultat au crible dans un billet intitulé « Anthropic m’a devancé ». Il a compilé les 13,4 millions de lignes, lancé un outil de comparaison indépendant et inspecté à la main le code non mathématique pour écarter toute exploitation d’un bug du vérificateur. Son verdict tient en trois nuances. La preuve suit l’exposé de Darmon, Diamond et Taylor de 1995, pas la démonstration moderne qu’il formalise lui-même. Elle ne couvre que les exposants premiers à partir de 17, ce qui suffit, les petits cas étant déjà traités. Et elle n’apporte « essentiellement aucune mathématique nouvelle », n’est pas lisible par un humain et met vingt fois plus de temps à compiler que Mathlib. Son projet, financé sur cinq ans à hauteur d’un million de livres, continue donc, avec un objectif qu’Anthropic n’a pas visé : une preuve documentée, réutilisable par la communauté. Il n’en conclut pas moins, cité par SiliconANGLE, que « les artefacts d’autoformalisation par IA sont désormais assez robustes pour qu’on bâtisse dessus ».

Un relecteur seul dans une bibliothèque, une loupe à la main, devant une pile de feuillets qui monte jusqu’au plafond — Kevin Buzzard a recompilé la preuve et inspecté le code lui-même : la relecture indépendante reste le travail humain qui compte.

Ce que ça change pour une PME

Vous ne formaliserez jamais un théorème. Mais le montage qui a marché ici est celui à copier pour confier une tâche longue à des agents, en trois règles :

Un juge automatique avant tout. Lean n’accepte pas un argument plausible, il compile ou il rejette. Pour vos propres agents, l’équivalent existe : un rapprochement comptable qui doit tomber juste, des tests qui passent, un contrôle de format sur chaque fiche produit. Sans critère vérifiable par une machine, laisser tourner un agent onze jours revient à accumuler des erreurs en silence.
Découper avant de lancer. Ce n’est pas le modèle qui a fait la différence entre l’échec et le succès, c’est le graphe de tâches de Prove2Me. Une mission longue se décompose en sous-tâches indépendantes, chacune avec un énoncé clair et un état visible par tous, comme les 50 agents de Toyota ont chacun leur périmètre.
Compter en tokens, pas en heures. Anthropic ne publie pas le coût de l’opération. Au tarif public de Fable 5.1, 50 $ le million de tokens en sortie, 6 milliards de tokens représenteraient de l’ordre de 300 000 $, hors remises et hors entrée. À l’autre bout de l’échelle, trois abonnements Claude Max ordinaires ont formalisé en trois jours le théorème de Vinogradov. La question n’est plus « est-ce possible ? » mais « quelle tâche vaut ce budget ? », et la grille à trois étages reste la bonne façon d’y répondre.

Claude a-t-il démontré le théorème de Fermat ?

Non. La démonstration est celle d’Andrew Wiles, publiée en 1995. Claude l’a traduite en Lean, un langage où l’ordinateur vérifie chaque étape, et c’est la première fois que cette traduction est complète. Le résultat confirme la preuve de Wiles, il ne la remplace pas.

Peut-on reproduire ce type de travail en entreprise ?

Pas à cette échelle. Le montage, lui, se transpose : une tâche longue découpée en sous-tâches, plusieurs agents en parallèle, un contrôle automatique qui accepte ou rejette chaque résultat, et un humain qui donne quelques consignes et relit à la fin.

Cette annonce ne montre pas qu’une IA devient mathématicienne, mais qu’une équipe d’agents bien outillée tient onze jours sur une tâche sans qu’on la tienne par la main, dès lors qu’une machine tranche à chaque pas. Concevoir ce montage pour ses propres processus, choisir le juge automatique et fixer le budget, c’est ce que travaillent les formations IA de Vincent Lévi. Si vous avez une tâche longue à confier à des agents, écrivez à l’équipe : la première étape est toujours de définir ce qui compte comme « réussi ».