Le dernier théorème de Fermat n’est plus un problème ouvert depuis la démonstration d’Andrew Wiles, publiée en 1995. Pourtant, un autre défi restait colossal : traduire toute la démonstration dans un langage qu’un ordinateur peut vérifier étape par étape.
Le 4 septembre 2026, Anthropic a annoncé que Claude avait réalisé cette formalisation de bout en bout en onze jours, avec l’aide d’une infrastructure multi-agent et de la plateforme Prove2Me.
Démontrer et formaliser : deux travaux différents
Une preuve destinée aux mathématiciens omet de nombreuses étapes considérées comme évidentes. Un assistant comme Lean ne laisse rien passer : les objets doivent être définis et chaque transition logique justifiée par un résultat disponible.
D’après Anthropic, les agents ont écrit environ 13 millions de lignes de Lean et prouvé plus de 30 000 théorèmes intermédiaires. La preuve finale s’appuie sur les axiomes standards de Lean et son énoncé a été comparé à celui de Mathlib.
Comment des dizaines d’agents ont coopéré
La taille du projet dépassait la mémoire pratique d’une seule conversation. Prove2Me a organisé le travail sous forme de graphe : chaque nœud représente un théorème à établir et les dépendances indiquent ce qui doit être terminé avant la suite.
Cette architecture a permis à plusieurs agents de :
- définir des concepts manquants ;
- tenter des preuves intermédiaires ;
- réutiliser des résultats déjà validés ;
- compiler séparément les composants ;
- remonter progressivement jusqu’au théorème final.
L’intervention humaine décrite par Anthropic était surtout stratégique : fixer certaines priorités et relancer les parties importantes. Les premières tentatives ont d’ailleurs échoué faute de coordination, ce qui montre que le modèle seul ne suffit pas ; l’organisation du travail compte énormément.
Pourquoi le résultat est important
L’intérêt immédiat n’est pas de redémontrer Fermat pour le plaisir. Une formalisation complète sert de test grandeur nature pour trois usages :
- Contrôler des preuves complexes, y compris celles proposées par d’autres IA.
- Construire des bibliothèques réutilisables de résultats vérifiés.
- Réduire la charge de vérification qui pèse sur les chercheurs et les rapporteurs.
Kevin Buzzard, qui anime un projet communautaire de formalisation du théorème, a examiné l’artefact et souligne son caractère réutilisable. Le dépôt étant publié, d’autres équipes peuvent l’auditer et en extraire des composants.
Les limites à garder en tête
Treize millions de lignes forment une preuve difficile à maintenir. Une formalisation certifiée peut être correcte tout en restant redondante, coûteuse ou peu pédagogique. Le prochain enjeu sera donc la compression : transformer une production massive en bibliothèque lisible et durable.
Enfin, Claude n’a pas remplacé Wiles. Sans la théorie élaborée par plusieurs générations de mathématiciens et sans les bibliothèques Lean existantes, cette formalisation n’aurait pas de fondation.
Source principale
- Anthropic — Formalizing Fermat’s Last Theorem, 4 septembre 2026.
FAQ
Claude a-t-il découvert une nouvelle preuve du théorème de Fermat ?
Non. Le travail formalise une voie issue de la preuve de Wiles et de développements ultérieurs. La nouveauté est l’automatisation et la vérification informatique de bout en bout.
Que vérifie Lean ?
Lean vérifie que les étapes formelles respectent les règles logiques et les axiomes déclarés. Cela ne rend pas automatiquement la preuve courte ou facile à lire pour un humain.