L'IA d'Anthropic formalise le dernier théorème de Fermat en Lean

Anthropic a publié une preuve complète et vérifiée par machine du dernier théorème de Fermat, écrite en Lean. L'entreprise affirme qu'un modèle de recherche interne l'a produite en 11 jours. Le résultat pèse environ cinq fois Mathlib, la principale bibliothèque ouverte de mathématiques formalisées.

Lean est un assistant de preuve. On écrit les mathématiques comme du code, et un petit programme appelé noyau vérifie chaque étape. Le dernier théorème de Fermat dit qu'aucun triplet d'entiers positifs a, b et c ne satisfait a^n + b^n = c^n lorsque n dépasse 2. Andrew Wiles l'a démontré en 1995. Personne n'avait encore écrit cette preuve sous une forme qu'une machine peut vérifier de bout en bout.

Ce que contient réellement le dépôt

L'article de recherche d'Anthropic est paru le 4 septembre 2026. Le code est sur GitHub sous licence Apache 2.0.

Son fichier README énonce le théorème formel. Pour des entiers positifs a, b et c, et tout n d'au moins 3, a^n + b^n n'est jamais égal à c^n.

Élément	Valeur
Chaîne d'outils Lean	4.33.1
Révision de Mathlib	v4.33.0
Théorèmes	29 511
Modules	60 475
Temps de compilation	5,5 heures avec 96 tâches parallèles
Pic de mémoire	230 Go
Taille de l'export	37,8 Go

Deux affirmations du README comptent plus que la taille. La preuve ne contient aucun sorry, l'espace réservé de Lean pour une étape que personne n'a terminée. Et elle repose sur trois axiomes seulement : propext, Classical.choice et Quot.sound. Ces trois-là sont livrés avec Lean. Rien de plus n'a été supposé pour refermer l'argument.

Anthropic indique que le modèle a démontré 30 300 théorèmes au total. Environ 29 500 se retrouvent dans la preuve finale. L'entreprise cite 6 milliards de jetons de sortie et 13 millions de lignes de Lean générées. Le travail est passé par Prove2Me, une plateforme qui découpe une formalisation en petits énoncés et les confie à des agents travaillant en parallèle.

Comment la preuve a été vérifiée

Trois vérifications distinctes ont eu lieu, et c'est la partie qui mérite qu'on s'y arrête.

Le noyau de Lean a d'abord accepté la preuve. Un outil nommé comparator, en version 4.33.0, l'a ensuite revérifiée en une quinzaine d'heures. Enfin Nanoda, un noyau indépendant écrit en Rust, a vérifié 1 052 234 déclarations en une trentaine de minutes.

Nanoda compte parce qu'il ne partage aucun code avec Lean. Un bogue dans le noyau de Lean ne serait pas attrapé par le noyau de Lean. Une seconde implémentation, dans un autre langage, est un vrai garde-fou contre ce risque.

Ce qu'en pensent les mathématiciens

Kevin Buzzard dirige le projet Xena. Il détient une subvention d'un million de livres du financeur de recherche britannique EPSRC, étalée sur cinq ans, pour formaliser précisément ce théorème. Il a écrit sur son blog qu'Anthropic est arrivé le premier.

Buzzard ne conteste pas le résultat. "Je suis sûr à 99,9 % que la preuve de FLT tient", a-t-il écrit. Sur la page d'Anthropic, il qualifie le travail de "réalisation d'autoformalisation extraordinaire".

Il trace aussi une limite. La formalisation "suit fidèlement la littérature ancienne sur la preuve et n'ajoute rien", a-t-il écrit. Elle reprend l'exposé de Darmon, Diamond et Taylor de 1995 sur l'argument de Wiles. Aucune mathématique nouvelle n'a été trouvée ici. Ce qui est nouveau, c'est que l'ancienne est désormais vérifiable par machine.

Buzzard note que la preuve couvre les nombres premiers d'au moins 17. Les nombres premiers irréguliers plus petits avaient déjà été formalisés par d'autres. Un commentateur de son billet, David Jao, a estimé le coût d'API de l'opération à environ 300 000 dollars.

Ce que cela signifie pour les développeurs

Si vous écrivez du Lean, vous pouvez cloner le dépôt, mais vérifiez d'abord votre matériel. Une compilation de 5,5 heures avec 96 tâches, et un pic mémoire de 230 Go, exclut presque tous les ordinateurs portables. Lisez plutôt la documentation HTML générée. Elle pèse 390 Mo et ne demande aucune compilation.

La leçon transposable n'est pas qu'un modèle a écrit 13 millions de lignes. C'est que personne n'a eu à les lire. Un noyau a tranché sur la correction du code, en quelques minutes, sans faire confiance à ce qui l'avait produit.

Cela ne marche que là où un vérificateur existe. Lean en a un. Votre service web, non. Avant d'en faire un modèle à suivre, demandez-vous ce qui jouerait le rôle du noyau dans votre propre pile. Un système de types, un test de propriétés ou un fuzzer sont les candidats habituels.

Si vous relisez du Lean écrit par une IA, deux contrôles mécaniques font l'essentiel du travail. Cherchez sorry, et affichez la liste des axiomes. L'affirmation d'Anthropic repose sur ces deux faits, et tous deux sont peu coûteux à confirmer vous-même.

L'écart de coût est le dernier point à noter. Produire la preuve a demandé 11 jours et des milliards de jetons. La revérifier dans un autre langage a demandé une demi-heure. Anthropic a déjà orienté des modèles de recherche vers le travail de laboratoire, et le même schéma tient ici. Produire coûte cher. Vérifier coûte peu.