Anthropic fait valider la preuve de Fermat par une armée d'agents Claude et par Lean
— AGENTS
Le théorème de Fermat était démontré depuis 1995 ; Anthropic a fait traduire cette démonstration en treize millions de lignes de code que le vérificateur Lean a contrôlées une à une. Onze jours de travail multi-agents révèlent surtout une infrastructure de coordination capable de faire tenir un chantier logique gigantesque sans perdre le fil.
Onze jours pour reconstruire une preuve qui a demandé trois siècles et demi de mathématiques. Ce chiffre impressionne, mais il ne dit rien d'une nouvelle vérité scientifique : Andrew Wiles et Richard Taylor avaient bouclé le dossier en 1995. Ce qu'Anthropic a produit, ce sont treize millions de lignes de code Lean qui rejouent cette démonstration en forçant chaque étape à se justifier devant une machine, sans raccourci ni sous-entendu.
Ce travail concerne d'abord les mathématiciens qui formalisent leur discipline, comme Kevin Buzzard et son équipe de l'Imperial College, engagés depuis des années sur ce même théorème. Leur objectif diffère de celui d'Anthropic : construire des briques réutilisables, documentées, capables d'entrer dans la bibliothèque Mathlib. Le dépôt produit par Claude, lui, ne sera pas maintenu et personne ne pourra y contribuer. Il prouve que la logique tient, sans offrir à un humain de quoi comprendre pourquoi elle tient.
La partie qui dépasse le cercle des mathématiciens tient dans l'organisation du travail. Des dizaines d'agents Claude ont collaboré via Prove2Me, une plateforme qui découpe un projet géant en un graphe de tâches, garde la trace de ce qui est validé et empêche les agents de repartir chacun de zéro sur la même étape. Les premières tentatives sans ce garde-fou avaient tourné court, les agents perdant la vue d'ensemble et multipliant les branches inutiles.
Cette mécanique de mémoire partagée, de relecture croisée entre agents et de vérification finale indépendante préfigure ce que les outils de production pilotés par agents devront résoudre ailleurs, dès qu'un studio confiera à plusieurs assistants automatisés un chantier trop vaste pour tenir dans une seule conversation : montage complexe, pipeline VFX, génération massive de variantes. La question n'est plus seulement la capacité d'un modèle à raisonner, elle devient celle de l'infrastructure qui distribue le travail sans le laisser dériver.
Le coût réel de l'opération reste flou. Anthropic ne communique ni le prix ni le nombre de machines mobilisées derrière les six milliards de tokens consommés, ce qui rend l'exploit spectaculaire mais difficile à situer par rapport à un budget ordinaire. Une expérience plus modeste, menée avec trois abonnements Claude standards sur un théorème plus petit, suggère que certains usages deviendront accessibles hors des grands laboratoires, sans garantir qu'une campagne de cette ampleur le devienne aussi.
Le prochain terrain de jeu n'est donc pas de battre un record de volume, mais de produire des chantiers formalisés plus courts et mieux organisés, pensés comme des outils de travail plutôt que comme des trophées de compilation.