Claude a-t-il vraiment démontré le théorème de Fermat ?

Ce qu’Anthropic a annoncé le 4 septembre

Anthropic affirme avoir produit avec Claude la première formalisation complète, de bout en bout et vérifiée par ordinateur du dernier théorème de Fermat. Le résultat est public : un dépôt rassemble le code Lean, le chemin de preuve, les outils de vérification et les instructions de compilation. L’annonce ne repose donc pas seulement sur une démonstration vidéo ou une capture d’écran ; un artefact technique peut être inspecté.

Selon Anthropic, des dizaines d’agents Claude ont travaillé pendant onze jours, largement de manière autonome, avec la plateforme collaborative Prove2Me et une orchestration fondée sur Claude Code. Ils ont produit environ 13 millions de lignes de Lean, démontré 30 300 théorèmes et utilisé 29 500 résultats intermédiaires dans la chaîne finale. Le projet aurait consommé près de six milliards de jetons de sortie.

Ces nombres donnent l’échelle du chantier, pas la qualité pédagogique du résultat. Ils proviennent principalement d’Anthropic et doivent être présentés comme tels. Le dépôt public permet de vérifier l’existence et la structure de l’artefact ; il ne permet pas à lui seul de confirmer chaque détail sur l’autonomie des agents ni le caractère mondialement inédit de l’ensemble.

Fait vérifiable : le code et les contrôles sont publics. Affirmation du fournisseur : il s’agit de la première formalisation complète de bout en bout, réalisée largement de façon autonome en onze jours.

Non, Claude n’a pas découvert une nouvelle preuve de Fermat

Le titre le plus spectaculaire serait aussi le moins précis. Le dernier théorème de Fermat a été démontré par Andrew Wiles, avec Richard Taylor pour la correction d’une difficulté, dans les années 1990. Le projet d’Anthropic suit une exposition simplifiée de cette voie due à Henri Darmon, Fred Diamond et Richard Taylor. Il transforme une argumentation mathématique connue en objets que Lean peut vérifier étape par étape.

Découvrir une preuve signifie trouver un raisonnement mathématique nouveau qui établit le résultat. Formaliser signifie expliciter dans un langage logique toutes les définitions, hypothèses et déductions nécessaires pour qu’un vérificateur puisse les contrôler. La formalisation peut exiger beaucoup d’inventivité : les textes humains omettent des étapes évidentes, utilisent des conventions implicites et s’appuient sur une vaste culture partagée. Mais l’innovation porte ici sur l’automatisation et la vérification, pas sur une nouvelle route mathématique vers le théorème.

Cette distinction ne diminue pas l’intérêt du travail. Elle évite simplement d’attribuer à un système une découverte qu’il n’a pas faite. Anthropic le dit lui-même : contrairement à certains travaux récents visant des résultats nouveaux, la nouveauté revendiquée ici est la vérification formelle d’un monument mathématique existant.

Ce que Lean vérifie réellement

Lean est à la fois un langage et un assistant de preuve. Une démonstration y devient une construction précise que le noyau du système vérifie selon des règles logiques restreintes. Le noyau n’accorde pas sa confiance au style, à la réputation de l’auteur ou à la fluidité d’une explication : si une étape ne correspond pas aux règles et aux hypothèses disponibles, le fichier n’est pas accepté.

Le dépôt d’Anthropic fixe Lean 4.33.1 et Mathlib 4.33.0. Mathlib fournit une bibliothèque communautaire de définitions et de théorèmes déjà formalisés. L’équipe indique que la preuve finale n’ajoute pas d’axiome, ne contient pas de trou de type « sorry », n’utilise pas de raccourci « native_decide » ni de code non sûr dans les modules de preuve. Un comparateur contrôle également que l’énoncé final correspond à celui du théorème de Fermat dans Mathlib.

Le contrôle a plusieurs étages : compilation par Lean, comparaison de l’énoncé et vérification par un noyau indépendant nommé nanoda. Cette défense en profondeur réduit le risque qu’un outil périphérique ou une convention de projet donne une impression de succès. Elle ne prouve toutefois pas que chaque nom, commentaire ou résumé en langage naturel décrit parfaitement l’objet formel. Le verdict porte sur l’énoncé encodé et la dérivation logique.

Pourquoi des dizaines d’agents ont été nécessaires

Une preuve de cette taille ne se résout pas comme une question isolée posée à un chatbot. Elle forme un graphe de dépendances : définir un objet, établir des lemmes, réutiliser ces lemmes et débloquer des résultats plus proches du but. Anthropic explique que les premières tentatives ont souffert d’une perte de contexte et d’une coordination insuffisante. Environ 7 % des lignes non standard de la version finale viendraient de ces essais.

Prove2Me a apporté une carte explicite des énoncés sous forme de graphe orienté, une séparation entre déclarations et preuves pour accélérer la compilation, ainsi qu’une couche de descriptions facilitant la recherche et la réutilisation. Chaque agent pouvait ainsi choisir une sous-tâche disponible sans devoir garder l’ensemble des 13 millions de lignes en mémoire.

La leçon dépasse les mathématiques. Pour les systèmes multi-agents, multiplier les assistants ne suffit pas. Il faut un état partagé, des interfaces stables, des critères de validation locaux et une façon de reconnecter chaque résultat au but final. Sans cette infrastructure, les agents peuvent produire beaucoup de texte ou de code sans faire progresser un projet cohérent.

Un résultat ouvert, mais difficile à reproduire

Le dépôt est publié sous licence Apache 2.0, ce qui permet de l’étudier et de le réutiliser selon les conditions de la licence. La publication mondiale facilite le contrôle par des spécialistes. Elle ne transforme pas pour autant l’expérience en exercice accessible à n’importe quel ordinateur portable.

La documentation mentionne environ 67 Go de stockage pour construire l’ensemble. Le contrôle approfondi par le Comparator peut demander jusqu’à 230 Go de mémoire vive, et certaines vérifications prennent longtemps. Les versions de Lean et de Mathlib sont épinglées : une reproduction sérieuse doit respecter cet environnement, enregistrer les commandes exécutées et distinguer une compilation partielle de la validation complète.

Ces contraintes comptent lorsque l’on parle d’ouverture. Un artefact téléchargeable est plus vérifiable qu’une affirmation fermée, mais une vérification indépendante reste un travail d’ingénierie. Les universités ou laboratoires qui l’examinent devraient publier les versions, ressources, journaux et éventuels écarts rencontrés afin que la confiance ne repose pas uniquement sur le communiqué initial.

Ce que cela change pour les étudiants et les enseignants

Pour l’apprentissage, la formalisation rend les implicites visibles. Un étudiant qui encode un petit résultat doit préciser le domaine des variables, les hypothèses et chaque transformation autorisée. Cette discipline peut révéler un raisonnement circulaire ou une condition oubliée. Elle complète bien une démonstration rédigée, surtout lorsque le retour du vérificateur sert à comprendre l’erreur.

Mais 13 millions de lignes ne constituent pas un manuel. Une preuve formelle peut être correcte tout en restant illisible pour une classe. L’enseignement doit conserver trois niveaux : l’intuition qui explique pourquoi le résultat est plausible, la preuve humaine qui organise les idées et la formalisation qui vérifie les détails. Supprimer l’un de ces niveaux appauvrit l’apprentissage.

L’usage responsable n’est pas de demander à Claude de rendre un devoir terminé. Il consiste à proposer sa propre démonstration, identifier une étape douteuse, formaliser un lemme limité et expliquer ensuite avec ses mots ce que le vérificateur a accepté. Les règles de l’établissement et la déclaration de l’aide utilisée restent applicables.

Cas pratique : vérifier un petit théorème sans déléguer son raisonnement

Prenons un étudiant qui veut vérifier que la somme de deux nombres pairs est paire. Il commence sur papier : si a = 2k et b = 2m, alors a + b = 2(k + m). Il liste les définitions nécessaires et écrit l’argument dans ses propres mots. Seulement ensuite, il crée un fichier Lean minimal avec la version imposée par son cours.

L’assistant IA peut expliquer un message d’erreur ou proposer une syntaxe, mais l’étudiant exige une justification pour chaque modification. Il compile après chaque petite étape, compare l’énoncé formel à l’énoncé français et garde l’historique. À la fin, il doit pouvoir refaire la preuve sans l’outil et expliquer la nature de chaque hypothèse.

Cette méthode utilise la machine comme banc de contrôle. Elle évite deux illusions : croire qu’un texte convaincant est forcément correct et croire qu’un fichier accepté suffit à démontrer que l’élève a compris. Pour un devoir évalué, l’étudiant demande au préalable quels usages de l’IA et du logiciel de preuve sont autorisés.

1. Écrire l’énoncé et la preuve humaine avant d’ouvrir l’assistant
2. Définir précisément les variables et hypothèses
3. Formaliser un lemme court dans une version fixée de Lean
4. Compiler après chaque étape et lire chaque erreur
5. Comparer l’énoncé formel à la phrase d’origine
6. Expliquer oralement la preuve sans recopier le code
7. Déclarer l’aide de l’IA selon les règles du cours

La grille en huit questions pour évaluer une annonce de mathématiques par IA

Les annonces combinent souvent résultat mathématique, performance d’un modèle et choix d’infrastructure. Séparez-les. Un dépôt public peut confirmer l’existence du code sans confirmer le coût exact, le degré d’autonomie ou l’antériorité mondiale. À l’inverse, une vérification indépendante solide peut avoir une grande valeur même si le raisonnement suit une preuve connue.

Cherchez d’abord l’énoncé exact et les hypothèses. Vérifiez ensuite si le résultat est nouveau, formalisé ou seulement reformulé. Identifiez le vérificateur, les axiomes, les trous admis, les dépendances et les versions. Enfin, demandez si une équipe extérieure a réellement reproduit le contrôle et si une explication destinée aux humains accompagne le code.

1. Quel énoncé exact a été vérifié ?
2. La preuve mathématique est-elle nouvelle ou déjà connue ?
3. Le code et les instructions sont-ils publics ?
4. Quelles versions, bibliothèques et hypothèses sont utilisées ?
5. Des trous, axiomes ajoutés ou raccourcis non sûrs restent-ils présents ?
6. Un noyau ou un outil indépendant a-t-il contrôlé le résultat ?
7. Une équipe extérieure l’a-t-elle reproduit avec des journaux publiés ?
8. Existe-t-il une explication humaine des idées principales ?

Les limites à garder en tête

Une preuve formelle vérifie ce qui a été encodé. Si l’énoncé ne correspond pas à la question que l’on croit poser, la machine peut certifier impeccablement la mauvaise cible. Le comparateur publié est donc important, mais les spécialistes doivent encore examiner les définitions, l’architecture et la fidélité mathématique du projet.

La taille est une autre limite. Treize millions de lignes générées sont difficiles à relire, à maintenir et à transmettre. Anthropic reconnaît que l’artefact est probablement beaucoup plus long que nécessaire. La prochaine étape utile n’est pas seulement de formaliser davantage : il faut réduire, structurer, documenter et produire des chemins de preuve compréhensibles.

Enfin, l’annonce vient du concepteur du système. Le dépôt élève le niveau de preuve, mais les affirmations « première mondiale », « largement autonome » et les mesures de ressources doivent être consolidées par des examens indépendants. Jusqu’à ces confirmations, il est raisonnable de parler d’un résultat public impressionnant, pas d’une validation définitive de toutes les promesses sur l’IA scientifique.

Verdict : une avancée de vérification, pas une nouvelle preuve de Fermat

Le résultat publié par Anthropic marque une étape importante pour l’autoformalisation à grande échelle. La combinaison d’agents, d’un graphe de dépendances, de Lean et de contrôles multiples montre qu’une IA peut convertir un vaste corpus mathématique connu en un artefact mécaniquement vérifiable beaucoup plus vite que les calendriers autrefois envisagés.

Il faut pourtant nommer correctement l’événement. Claude n’a pas remplacé Wiles et n’a pas découvert une preuve inédite. Il a participé à la formalisation massive d’une route connue, sous une infrastructure conçue par des humains et avec des contrôles formels. C’est déjà considérable : à mesure que les IA produisent davantage de mathématiques, la capacité à vérifier systématiquement leurs résultats pourrait devenir aussi importante que leur capacité à proposer des idées.