Anthropic a publié le 4 septembre une formalisation vérifiée par la machine du dernier théorème de Fermat dans Lean 4 ; l'API GitHub date la création du dépôt de 14:21:04 UTC. L'affirmation qui a circulé était que Claude avait prouvé le dernier théorème de Fermat en 11 jours. Les propres fichiers du dépôt décrivent quelque chose de plus étroit et, à un autre égard, de plus intéressant.

Ce que dit le fichier d'attribution

Le dépôt fournit un ATTRIBUTION.md recensant 106 fichiers contenant du matériel issu du projet FLT de l'Imperial College London dirigé par Kevin Buzzard et du projet flt-regular — « 54 sous Definitions/, 52 sous P2M/Sol/ ; et les 23 fichiers qui reproduisent le texte de Mathlib ». Des dizaines de lignes indiquent « whole file (100%) ». Le fichier NOTICE date l'emprunt : « Material was taken from the project's main branch as of 2026-05-21 ». Lors du portage de la chaîne d'outils vers Lean 4.33, le fichier d'attribution indique qu'il « left the other 41 byte-identical ».

La vérification est réelle

Rien de tout cela n'invalide la vérification. Le README indique que les 60 475 modules ont tous été compilés, que #print axioms fermat_last_theorem est limité aux trois axiomes standard, et qu'aucun module ne contient axiom, sorry, native_decide, unsafe ou partial def. La compilation a pris 5 heures 32 minutes avec 96 jobs, avec un pic de 153 Go de mémoire. Chiffres d'Anthropic : 13 millions de lignes de Lean, 29 500 théorèmes intermédiaires utilisés dans la preuve finale, environ six milliards de jetons de sortie.

Ce que le cadrage retenu ne dit pas correctement

Trois choses. Claude n'a rien prouvé de nouveau — il s'agit d'une autoformalisation de l'exposition de 1995 de Darmon, Diamond et Taylor de l'argument de Wiles, Taylor et Wiles, une preuve achevée par des humains il y a trente et un ans. Ce n'est pas sans assistance : selon le propre décompte d'Anthropic, un neuvième du dépôt contient du texte Lean humain, parfois repris mot pour mot. Et Buzzard, le mathématicien dont Anthropic cite la revue, a écrit le même jour sur son blog que « mathematically this work of anthropic tells us essentially nothing » et que la formalisation « just faithfully follows the early literature on the proof and adds nothing ». Plusieurs médias ont aussi parlé du plus grand fichier de ce type ; il s'agit de 60 475 modules, pas d'un fichier.

La revendication honnête reste malgré tout considérable

Les machines peuvent désormais traduire des milliers de pages de littérature mathématique existante en forme vérifiable par le noyau en moins de deux semaines, à partir de plusieurs années de travail bénévole en Lean. C'est un vrai résultat sur la vitesse de traduction. Ce n'est pas un résultat sur la découverte mathématique, et le README reconnaît lui-même l'écart qui subsiste : « What no tool can check is that each intermediate theorem means what its name suggests. »