AIREITERQuand un titre annonce que « Claude a résolu le dernier théorème de Fermat », un mot mérite toute votre attention : formalisé. Anthropic a publié un artefact Lean accessible au public, présenté comme une vérification complète du théorème. Mais le chemin mathématique reste celui, bien connu, de Frey–Serre–Ribet–Wiles–Taylor-Wiles — pas une preuve nouvelle découverte par l’IA.
Commencer par distinguer les deux affirmations
La réponse courte est oui : Anthropic a publié un dépôt contenant une formalisation en Lean 4 du dernier théorème de Fermat (FLT), avec des instructions pour le compiler et le vérifier. En revanche, dire que Claude a résolu seul ce problème mythique serait inexact : la percée mathématique revient à Andrew Wiles et Richard Taylor, plusieurs décennies plus tôt.
Le FLT affirme qu’il n’existe aucune solution en entiers positifs à a^n + b^n = c^n lorsque n > 2. Publiée en 1995, la preuve de Wiles est ici transformée en artefact vérifiable par une machine. Pour le contexte historique, consultez l’annonce du projet FLT par la communauté Lean.
Une preuve Lean ne répond pas à la même question qu’un article mathématique rédigé en langage naturel. Elle peut établir qu’une proposition encodée avec précision découle de définitions, de dépendances et d’axiomes vérifiés dans un environnement donné. Elle ne prouve ni qu’une IA a inventé les mathématiques sous-jacentes, ni que les noms des théorèmes correspondent réellement à leur contenu.
Ce qu’Anthropic a réellement publié
Dans son billet de recherche du 4 septembre 2026, Anthropic affirme que Claude a produit la première formalisation Lean complète et vérifiée par ordinateur du FLT, de bout en bout, en 11 jours. La publication fait état d’environ 13 millions de lignes de Lean, de 30 300 énoncés de théorèmes démontrés, dont 29 500 utilisés dans la preuve finale. Elle mentionne également près de 6 milliards de tokens générés.
Le travail s’appuie sur Prove2Me, une plateforme qu’Anthropic décrit comme gérant un graphe orienté acyclique d’énoncés mathématiques et coordonnant plusieurs agents. Selon Anthropic, la formalisation suit une présentation simplifiée de la preuve établie associée à Frey, Serre, Ribet, Wiles et Taylor-Wiles.
Pour vérifier l’affirmation, le dépôt GitHub est plus utile que l’annonce. Sa cible par défaut est FinalCheck.lean, qui contient la déclaration suivante :
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nLe dépôt se présente comme un artefact de recherche non maintenu et n’acceptant pas les contributions. Il verrouille Lean 4.33.1 et Mathlib v4.33.0, inclut PROOF-PATH.md et fournit une version HTML consultable hors ligne de l’arbre des théorèmes et des définitions.
La vérification finale du dépôt est conçue pour échouer si la preuve dépend d’un axiome ajouté, de sorry, de native_decide, de unsafe ou d’une autre échappatoire similaire. L’artefact peut donc être inspecté directement : il ne s’agit pas de faire confiance à une capture d’écran ou à un simple résumé.
Comment reproduire la vérification
Une vérification sérieuse commence par l’environnement verrouillé du dépôt, pas par la copie d’un fichier .lean isolé dans un autre projet. Le guide de vérification de la communauté Lean explique pourquoi : Lean sort une nouvelle version chaque mois, Mathlib évolue fréquemment et la compatibilité ascendante n’est pas garantie.
Verrouiller l’environnement avant la compilation
Le dépôt indique que la compilation est prévue pour Linux ou macOS et nécessite elan, Git, Python, GNU coreutils ainsi qu’une connexion réseau afin que Lake puisse récupérer et compiler les dépendances verrouillées. Il faut compter environ 67 Go dans .lake, auxquels s’ajoutent près de 220 Go de fichiers C générés, que l’on peut supprimer ensuite.
Le dépôt indique également environ 5 Go de mémoire par tâche parallèle, certains modules pouvant nécessiter jusqu’à 36 Go. Avec 96 tâches, sa propre compilation a duré 5 heures 32 minutes et atteint un pic de 153 Go de mémoire. Ces chiffres sont ceux communiqués par le dépôt, pas des mesures réalisées pour cet article : considérez-les comme un avertissement pour dimensionner la machine, et non comme une durée garantie.
Choisir son niveau de vérification
- Se contenter d’inspecter : lire
FinalCheck.lean,PROOF-PATH.mdetATTRIBUTION.mdsans compiler. - Compiler entièrement avec Lean : utiliser la toolchain verrouillée et lancer
lake build. - Rejouer la preuve indépendamment : après une compilation et une exportation réussies, exécuter les scripts comparator et nanoda.
Depuis un clone vierge, le dépôt propose globalement la séquence suivante :
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build
# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh
# Run after the comparator check.
verification/nanoda/run.shCes étapes n’ont pas le même objectif :
| Étape | Détail communiqué par le dépôt | Objectif |
|---|---|---|
lake build | 60 475 modules ; 5 h 32 min avec 96 tâches lors de l’exécution indiquée | Compile le projet depuis ses sources et permet au noyau Lean de vérifier les déclarations incluses dans la compilation |
| Comparator | 14 h 46 min lors de l’exécution indiquée ; pic de mémoire de 230 Go | Vérifie que le théorème exposé et les constantes référencées correspondent à l’énoncé de référence utilisé dans Mathlib |
nanoda | Environ 30 minutes avec 16 threads après l’export | Rejoue un environnement exporté au moyen d’un noyau Lean indépendant écrit en Rust |
Le comparator ne remplace pas la lecture de l’énoncé du théorème. Il aide à écarter le risque qu’un projet démontre une proposition affaiblie ou subtilement différente. Le PROOF-PATH.md du dépôt fait correspondre les étapes mathématiques nommées aux déclarations Lean, tandis que les pages HTML générées permettent d’inspecter les dépendances sans lancer d’application web.
Le dépôt indique aussi des coûts supplémentaires pour les deux vérifications : l’écriture d’un export de 37,8 Go peut nécessiter environ 90 Go de mémoire, et le workflow nanoda peut demander environ 40 Go pendant la vérification.
Ce que les vérifications établissent — et leurs limites
| Niveau de preuve | Ce qu’il établit | Ce qu’il n’établit pas |
|---|---|---|
| Compilation par le noyau Lean | Les termes de preuve soumis sont correctement typés dans l’environnement Lean verrouillé | Que Claude a découvert les mathématiques, ou que l’explication informelle correspond à chaque nom de théorème |
FinalCheck.lean et garde-fou sur les axiomes | Le théorème final du dépôt est vérifié par rapport à la liste d’axiomes indiquée et rejette plusieurs raccourcis répertoriés | Que le théorème correspond bien à l’énoncé historique du FLT si l’énoncé lui-même n’est pas inspecté |
Sortie de #print axioms | Lorsque la vérification attendue réussit, les dépendances incluent les trois axiomes standards de Lean — propext, Classical.choice et Quot.sound — plutôt qu’un axiome utilisateur caché | Que l’ensemble de la chaîne logicielle a été validé indépendamment |
| Comparator | Le résultat démontré et les constantes référencées correspondent au défi limité à Mathlib utilisé par le dépôt | Que toutes les descriptions en langage naturel du projet sont claires ou pédagogiquement satisfaisantes |
| Rejeu nanoda | Un environnement exporté a été accepté par une seconde implémentation du noyau Lean, écrite en Rust | Que l’export, les scripts ou le système d’exploitation sont à l’abri de toute erreur possible |
PROOF-PATH.md et attribution | Un parcours permettant aux humains d’examiner la correspondance mathématique et les sources antérieures | Que les noms de théorèmes générés par machine décrivent correctement leurs énoncés sans revue humaine |
La checklist « Did you prove it? » de la communauté Lean rappelle la règle essentielle : la compilation valide la proposition encodée, pas l’adéquation entre le nom d’un théorème et l’affirmation informelle qu’il est censé représenter. Dans cet artefact, le comparator et son utilisation de Mathlib réduisent ce risque, mais ne dispensent pas de lire la déclaration du théorème et le parcours de preuve.
Ce que l’artefact démontre — et ce qu’il ne démontre pas
Le système a produit un artefact Lean formellement vérifié, d’une ampleur inhabituelle. Cela ne démontre ni l’existence d’une nouvelle voie vers le FLT, ni celle d’une nouvelle preuve élémentaire, ni une découverte mathématique indépendante réalisée par Claude.
Anthropic affirme que la preuve suit une version simplifiée de l’approche de Wiles. Le dépôt crédite également des travaux existants : son fichier ATTRIBUTION.md identifie 106 fichiers contenant du matériel issu du projet FLT de l’Imperial College London ou de flt-regular, en plus de Mathlib. Cette provenance est indispensable pour décrire correctement les fondations de l’artefact publié.
Le projet fait état de 30 300 énoncés de théorèmes démontrés pendant l’exécution et d’environ 29 500 utilisés dans la preuve finale, tandis que le dépôt décrit 29 511 pages de théorèmes. Il s’agit de déclarations formelles et de dépendances, pas de 29 511 résultats mathématiques nouvellement découverts. Une preuve formelle explicite les étapes implicites, les types, les coercitions, les définitions et les dépendances de bibliothèque qu’une démonstration humaine peut laisser à la compréhension d’un spécialiste.
Le dépôt précise que ses sources ont été écrites pour être vérifiées, pas pour être lues : les noms sont générés par machine, les étiquettes comme P2M correspondent au pipeline, et c’est l’énoncé — non le nom — qui fait foi. Voilà pourquoi le parcours de preuve et le comparator comptent autant que le théorème mis en avant.
Les travaux Lean antérieurs ne doivent pas être fondus dans l’affirmation de 2026. Un article de 2023 consacré au dernier théorème de Fermat pour les nombres premiers réguliers faisait état d’une formalisation complète, sans sorry, du cas I du théorème de Kummer pour les nombres premiers réguliers, tout en précisant que le cas II et le lemme de Kummer restaient des chantiers importants. Une révision publiée en 2025 présentait cette formalisation des nombres premiers réguliers comme une preuve complète de ce cas plus limité.
| Travail | Périmètre | Rôle pratique |
|---|---|---|
Recherche flt-regular | Résultats sur les nombres premiers réguliers et infrastructure d’appui en théorie algébrique des nombres | Brique formelle antérieure et matériel source |
| Projet FLT de l’Imperial | Formalisation durable et réutilisable de la théorie moderne des nombres autour du FLT | Infrastructure de bibliothèque et de collaboration |
| Dépôt Anthropic | Théorème FLT de bout en bout revendiqué en Lean 4, avec vérifications de compilation et de rejeu | Artefact de recherche de grande ampleur, optimisé pour obtenir un résultat vérifié plutôt que pour être maintenu sur le long terme |
Le projet FLT de l’Imperial et de Lean présente la formalisation de la théorie moderne des nombres comme un effort d’infrastructure plus large, et non comme la simple traduction d’un théorème. La publication d’Anthropic doit plutôt être vue comme un élément complémentaire sur les capacités d’agents IA coordonnés au sein d’un écosystème formel existant, pas comme la preuve que les objectifs du projet précédent seraient devenus inutiles.
À quel niveau accorder sa confiance ?
| Si vous cherchez à savoir… | La réponse rigoureuse est… | Étape suivante |
|---|---|---|
| Si Anthropic a publié un véritable artefact | Oui ; il existe une annonce officielle et un dépôt public dont l’environnement est verrouillé | Lire ensemble le billet de recherche et le dépôt |
| Si le théorème encodé est bien le FLT | Le dépôt fournit une déclaration précise, un comparator et un parcours de preuve | Inspecter FinalCheck.lean, le comparator et PROOF-PATH.md |
| Si le code se compile correctement | Le dépôt documente une compilation depuis zéro et en rapporte le résultat | Recompiler avec Lean 4.33.1 et Mathlib v4.33.0 si vous disposez du matériel nécessaire |
| Si Claude a inventé une nouvelle preuve | Aucun élément ne permet de le dire ; la voie suivie repose sur les mathématiques établies de Wiles et Taylor-Wiles | Parler de formalisation ou d’ingénierie de preuve assistée par IA |
| Si l’artefact est facile à maintenir | Non ; le dépôt se décrit explicitement comme non maintenu et son code est généré par machine | Le considérer comme un artefact de recherche, pas comme une bibliothèque Mathlib prête à l’emploi |
| Si cela prouve l’autonomie mathématique générale | Non ; le résultat montre des performances sur une cible de formalisation très spécifiée, avec un échafaudage conséquent | Distinguer la capacité de vérification formelle de la découverte de théorèmes en terrain ouvert |
Si vous cherchez simplement l’information, la publication officielle et le dépôt suffisent à établir que le projet existe. Si vous devez l’auditer, reproduisez la compilation verrouillée et examinez l’énoncé. Pour évaluer la recherche en IA, prenez en compte l’orchestration, les bibliothèques existantes, les formalisations antérieures et les ressources de calcul : ils font partie intégrante du système.
FAQ
Claude a-t-il découvert une nouvelle preuve du dernier théorème de Fermat ?
Non. L’artefact d’Anthropic formalise une voie de preuve établie, associée à Frey, Serre, Ribet, Wiles et Taylor-Wiles. La performance réside dans l’échelle et la rapidité de production d’un artefact Lean vérifiable par machine, pas dans une nouvelle solution mathématique.
Une compilation Lean réussie prouve-t-elle le théorème informel ?
Elle prouve que la proposition encodée découle des dépendances vérifiées dans cet environnement Lean. Il faut encore vérifier que la proposition et ses définitions correspondent bien au théorème informel que vous souhaitez revendiquer.
Le dépôt utilise-t-il sorry ou des axiomes supplémentaires ?
Le dépôt indique que sa vérification finale rejette sorry, les axiomes ajoutés, native_decide, unsafe et plusieurs raccourcis apparentés. La liste d’axiomes attendue contient les trois axiomes standards de Lean : propext, Classical.choice et Quot.sound ; reproduisez la vérification au lieu de vous fier uniquement à l’annonce.
Puis-je reproduire le résultat sur un ordinateur portable classique ?
Vous pourrez peut-être inspecter le dépôt et en compiler une partie, mais la vérification complète n’est pas une opération légère destinée à une machine ordinaire. Le dépôt rapporte un pic de mémoire de 153 Go pour sa compilation, jusqu’à 230 Go pour le comparator et d’importants besoins en stockage : le matériel constitue donc une contrainte centrale.
Pour évaluer correctement l’affirmation, commencez par l’artefact GitHub verrouillé, lisez la déclaration du théorème avant de vous arrêter au titre et présentez le résultat comme une vaste formalisation assistée par IA de mathématiques connues.