Le dernier théorème de Fermat affirme que xⁿ + yⁿ = zⁿ n'a pas de solution en nombres entiers positifs quand n est supérieur à 2. Pierre de Fermat l'a griffonné dans une marge vers 1630 ; Andrew Wiles l'a démontré dans les années 1990 avec certaines des mathématiques les plus difficiles jamais écrites. Le 4 septembre 2026, Anthropic a annoncé que Claude avait produit en 11 jours la première version complète vérifiée par ordinateur de cette preuve[1]. Cet article explique ce que cela signifie, pourquoi c'est autant une histoire d'informatique que de maths, et ce que cela ne signifie pas.
Chronologie
- années 1630Fermat affirme avoir une preuve que « cette marge est trop étroite pour contenir ».
- 1994–95Andrew Wiles (avec Richard Taylor) achève la preuve.
- 2024Kevin Buzzard lance à l'Imperial College de Londres un projet humain de formalisation de la preuve dans Lean.
- août 2026Des agents Claude achèvent une formalisation complète dans Lean en 11 jours.
- 4 sept. 2026Anthropic annonce le résultat ; Buzzard le relit.
Ce que fait un assistant de preuve
Tronc commun GCSE
Une preuve écrite par un humain laisse de petites étapes au lecteur. Même des relecteurs experts peuvent manquer une lacune. Un assistant de preuve comme Lean élimine ce risque. On écrit définitions et preuves sous forme de code, et un petit vérificateur de confiance (le noyau) confirme que chaque étape découle de la logique et des résultats antérieurs. Si le code compile, le théorème est vérifié. C'est comme un compilateur qui refuse d'exécuter votre programme tant qu'il n'est pas démontré correct.
Une preuve formelle est un arbre : le théorème final repose sur de grands résultats intermédiaires, qui reposent sur des lemmes, qui reposent sur des définitions et des faits de base. Lean vérifie chaque lien. Appuyez sur le bouton pour vérifier l'arbre à partir des fondations. Schéma ; le vrai arbre compte environ 29 500 théorèmes.
Ce que Claude a réellement fait
Approfondissement A-Level
- Il a formalisé une version simplifiée de la preuve de Wiles, due à Darmon, Diamond et Taylor[1].
- Le résultat compte environ 13 millions de lignes de Lean et environ 30 300 théorèmes (environ 29 500 utilisés dans la preuve finale), soit plus de cinq fois la taille de Mathlib[1].
- Des dizaines d'agents Claude ont travaillé en parallèle pendant 11 jours, en utilisant environ six milliards de jetons de sortie d'un modèle de recherche interne[1].
- L'apport mathématique humain s'est limité à des instructions ponctuelles de haut niveau du chercheur d'Anthropic Tianyi Peng[1].
- La preuve ne repose que sur les trois axiomes standard de Lean, et un comparateur a confirmé que le théorème final énonce exactement ce que dit l'énoncé du dernier théorème de Fermat dans Mathlib[1].
- Elle a réutilisé des éléments du projet FLT de Kevin Buzzard à l'Imperial College de Londres, et Buzzard a relu la preuve achevée[1].
Vérification rapide
Que signifie le fait que la preuve « compile » dans Lean ?
Pourquoi vérifier l'énoncé compte
Une preuve vérifiée par ordinateur n'est utile que si elle démontre le bon énoncé. Si le théorème était légèrement mal écrit dans Lean, une preuve parfaite de la mauvaise chose ne vaudrait rien. C'est pourquoi l'équipe a utilisé un comparateur pour confirmer que l'énoncé correspond à la version écrite indépendamment dans Mathlib, et pourquoi le contrôle « aucun axiome supplémentaire » compte : il montre que rien n'a été simplement supposé[1]. Vérifier les étapes et valider la spécification sont deux tâches distinctes, exactement comme en test logiciel.
La distinction que les élèves confondent souvent
Correct ne veut pas dire élégant (ni nouveau).
Question type examen
Expliquez la différence entre vérification et validation, en prenant la preuve formelle du dernier théorème de Fermat comme exemple. [4 points]
Afficher la réponse modèle et le barème
- la vérification contrôle que le produit est construit correctement, c'est-à-dire qu'il respecte sa spécification (1 point)
- ici, Lean vérifie que chaque étape de la preuve est logiquement correcte (1 point)
- la validation contrôle qu'on a construit le bon produit, c'est-à-dire que la spécification correspond à ce qui était réellement voulu (1 point)
- ici, comparer l'énoncé Lean avec l'énoncé indépendant de FLT dans Mathlib vérifie que la preuve démontre bien le théorème visé (1 point)
Ce que vérifie l'examinateur : définir les deux termes et rattacher chacun à une partie précise de l'exemple.
Erreur fréquente : traiter les deux mots comme des synonymes. Un programme peut passer tous les contrôles de vérification et faire quand même la mauvaise chose.
Logique, preuve et tests relient maths et informatique en A-Level. Notre article L'IA sait-elle vraiment faire des maths ? donne une vue d'ensemble, et les problèmes du prix du millénaire montrent quelles questions restent ouvertes.
Sources et pour aller plus loin
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — échelle, agents, axiomes, apport humain, relecture de Buzzard, réserves
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — couverture médiatique
- Lean community: Mathlib — la bibliothèque mathématique de Lean
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — le projet mené par des humains
Dernière relecture : 5 octobre 2026. Les chiffres sont des valeurs publiées typiques et les règles peuvent changer. La formulation des examens varie selon la spécification : vérifiez la vôtre.
Questions fréquentes
Une IA a-t-elle démontré le dernier théorème de Fermat ?
Non : Andrew Wiles l'a démontré dans les années 1990. En 2026, des agents Claude ont traduit une version de cette preuve dans Lean, un langage de programmation dont le vérificateur contrôle chaque étape logique. Le résultat, annoncé par Anthropic le 4 septembre 2026, est la première preuve complète du théorème vérifiée par ordinateur.
Qu'est-ce que Lean ?
Un assistant de preuve : un langage de programmation dans lequel définitions, théorèmes et preuves s'écrivent comme du code. Un petit programme de confiance, le noyau, vérifie que chaque étape découle des règles de la logique et des résultats antérieurs. Si la preuve compile, le théorème est vérifié, en supposant seulement les axiomes intégrés à Lean.
Quelle est la taille de la preuve ?
Environ 13 millions de lignes de code Lean et quelque 30 000 théorèmes (environ 29 500 utilisés dans la preuve finale), soit plus de cinq fois la taille de Mathlib, la principale bibliothèque mathématique communautaire de Lean. Il a fallu 11 jours, avec des dizaines d'agents Claude travaillant en parallèle et des indications ponctuelles de haut niveau du chercheur d'Anthropic Tianyi Peng.
La preuve écrite par l'IA est-elle bonne ?
Elle est correcte au sens où Lean l'a vérifiée, et Kevin Buzzard, qui dirige le projet humain de formalisation de FLT à l'Imperial College de Londres, l'a relue. Mais Anthropic dit qu'elle est probablement bien plus longue que nécessaire, et que des tentatives ratées ont laissé environ 7 % de ses lignes hors code standard. Correct et élégant sont deux choses différentes.
Notes et avis des lecteurs
Notez cet article sur plusieurs aspects — votre avis aide les autres lecteurs, et nous aide à nous améliorer.
Cet article vous a-t-il été utile ?
Dites-nous ce que vous en pensez — une correction, une question restée sans réponse, ou un sujet que vous aimeriez voir traité ensuite.
Vous préférez en parler ? Réservez un appel vidéo gratuit au moment qui vous convient : 15 minutes pour une question rapide, 30 pour le reste. Les horaires s'affichent dans votre fuseau horaire.
À propos de l'auteur
Sudershan Soni
Fondateur et tuteur principal chez Mostak Services — tuteur de mathématiques, sciences, informatique et STEM titulaire d'un Master, avec plus de 20 ans d'expérience professionnelle, enseignant à des élèves du 11+ et du GCSE jusqu'à l'A-Level et au-delà, en ligne dans le monde entier.
Lire le profil complet