Selon Anthropic, son IA Claude a produit la première preuve entièrement vérifiée par ordinateur du dernier théorème de Fermat, en accomplissant ce travail en 11 jours, en grande partie seule, et en rédigeant ce qui est désormais la plus longue démonstration mathématique jamais construite.

Un projet humain mené à l'Imperial College London travaille sur exactement la même tâche depuis 2024 et n'est pas près d'être terminé. Claude l'a devancé. Kevin Buzzard, le mathématicien qui dirige le projet de l'Imperial, a examiné la preuve de Claude et a confirmé qu'elle tient debout en n'utilisant rien de plus que les règles logiques les plus élémentaires des mathématiques.

D'après Anthropic, Claude a rédigé la plus longue démonstration mathématique jamais réalisée et l'a utilisée pour prouver formellement le dernier théorème de Fermat, un problème qui a dérouté les mathématiciens pendant 358 ans. L'IA y est parvenue en 11 jours, pour l'essentiel seule, en produisant 13 millions de lignes de code qu'un ordinateur peut vérifier ligne par ligne, au lieu d'exiger la confiance accordée à la parole d'un mathématicien.

Le dernier théorème de Fermat affirme qu'il n'existe pas trois nombres entiers positifs qui, élevés chacun à une puissance supérieure à 2, puissent voir les deux premiers s'additionner pour donner le troisième. Pierre de Fermat a griffonné cette affirmation en marge d'un livre de mathématiques en 1637, ajoutant qu'il disposait d'une « démonstration vraiment merveilleuse » que la marge était trop étroite pour contenir. Puis il est mort. Les mathématiciens ont passé les 358 années suivantes à tenter de reconstituer ce qu'il pensait avoir trouvé.

Prouver quelque chose et le vérifier sont deux tâches différentes

Une démonstration mathématique est une chaîne d'étapes logiques, et si un seul maillon est brisé, tout s'effondre. Trouver ce maillon défectueux, enfoui quelque part dans une centaine de pages d'argumentation dense, peut coûter des années de travail à d'autres mathématiciens.

Formaliser une preuve signifie la traduire dans un langage si littéral qu'un ordinateur peut vérifier chaque étape de lui-même, sans entrer dans des subjectivités.

Les mathématiciens ont longtemps eu du mal avec la vérification. Un prix allemand de 1908 — d'une valeur d'environ 1 à 2 millions de dollars actuels, offert pour la première démonstration valide du théorème — a attiré 621 soumissions erronées dès sa première année.

Comme Anthropic l'a écrit sur X :

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

La véritable démonstration n'est apparue qu'en 1995, du mathématicien britannique Andrew Wiles, et elle a connu un rebondissement. Wiles a annoncé sa solution lors de trois conférences en juin 1993, avant qu'un relecteur n'y découvre plus tard une faille. Il a passé près d'un an à la corriger avec un ancien étudiant, Richard Taylor, a failli renoncer, et a finalement publié une preuve corrigée de 129 pages en mai 1995. Elle reposait sur des mathématiques qui n'existaient pas du temps de Fermat, ce qui explique en grande partie pourquoi les mathématiciens doutent aujourd'hui que la « démonstration merveilleuse » de Fermat ait jamais réellement fonctionné.

Les mathématiques vérifiées par ordinateur existent depuis des décennies. Le premier cas célèbre fut la démonstration assistée par ordinateur du théorème des quatre couleurs en 1976, qui a déclenché un débat toujours en cours sur la question de savoir si une preuve qu'aucun humain ne peut lire intégralement à la main doit compter. Les langages de preuve formelle comme Lean — créé par Leonardo de Moura, initialement chez Microsoft Research — sont nés précisément de cette tension, en laissant le logiciel faire la vérification pour que les humains puissent quand même faire confiance au résultat.

En 2024, Kevin Buzzard, mathématicien à l'Imperial College London, a lancé un projet pour faire exactement ce que Claude vient d'accomplir : traduire la preuve de Wiles en Lean, un langage que les ordinateurs peuvent vérifier. C'est le genre de tâche qui exige une armée de mathématiciens bénévoles — le plan du projet s'étend lui-même sur 86 pages, et son financement est assuré jusqu'en 2029. Claude a terminé l'ensemble en 11 jours.

Comment Claude y est réellement parvenu

Anthropic explique dans un article plus détaillé que Tianyi Peng, qui développe des outils de formalisation par IA avec une équipe à Columbia, a décidé de voir jusqu'où Claude pouvait aller seule. Des dizaines d'agents Claude ont travaillé en parallèle, rédigeant des définitions, prouvant de petits résultats et les empilant en résultats plus vastes, avec presque aucune intervention humaine au-delà d'occasionnelles incitations du type « donner la priorité à ce théorème ensuite ».

Tout ne s'est pas déroulé sans accroc au début. Les agents perdaient régulièrement le fil de ce qu'ils avaient déjà prouvé et cessaient de collaborer ; ces fausses pistes représentent encore environ 7 % des lignes de la preuve finale.

Ce qui a corrigé le problème, c'est un outil appelé Prove2Me, également développé par l'équipe de Peng, qui donnait à chaque agent la même liste de tâches en temps réel indiquant quelles preuves secondaires restaient à faire, afin que personne ne duplique le travail ni ne s'égaîne. Il organisait aussi les fichiers pour que Lean vérifie tout plus rapidement, et tenait des notes en anglais simple sur chaque résultat afin que les agents puissent réutiliser le travail des autres au lieu de réinventer.

Une fois terminé, Claude avait prouvé plus de 30 000 théorèmes auxiliaires et consommé des milliards de tokens, en tournant sur un modèle de recherche qu'Anthropic dit à peu près comparable à Claude Fable 5.1, la version qu'elle a ensuite rendue publique. La preuve finale compte 13 millions de lignes — plus de cinq fois la taille de Mathlib, la bibliothèque partagée que les mathématiciens utilisent déjà pour ce type de travail.

Un roman type compte 80 000 mots. La preuve de Claude équivaut à 160 romans de pure argumentation logique.

Est-ce que cela compte vraiment ?

Buzzard — dont la propre version de ce projet reste financée jusqu'en 2029 — a examiné la preuve de Claude et lui a donné sa bénédiction, déclarant qu'elle démontre le théorème « sans aucune autre hypothèse que les axiomes des mathématiques ».

Il ne s'agit pas d'une découverte de mathématiques entièrement nouvelles par Claude, ce qu'Anthropic a également revendiqué cette année avec sa recherche en cryptographie. Wiles avait déjà prouvé le théorème de Fermat il y a trois décennies — Claude a simplement construit un reçu vérifiable par machine. C'est important parce que les mathématiciens sont de plus en plus submergés de preuves non vérifiées, y compris écrites par des IA, arrivant plus vite que les humains ne peuvent les vérifier à la main. Ces preuves formalisées sont également déterministes et moins sujettes aux erreurs humaines, ce qui est très important en mathématiques.

Ce n'est pas un problème nouveau. Une preuve assistée par ordinateur de la conjecture de Kepler a pris quatre ans avant qu'un comité de lecture ne s'engage qu'à être « certain à 99 % », et la démonstration de la conjecture de Poincaré par Grigori Perelman a mis environ autant de temps à être pleinement assimilée.

Quiconque ne veut pas croire Anthropic sur parole n'y est pas obligé. La preuve complète de 13 millions de lignes est disponible sur GitHub, libre d'accès pour tout mathématicien disposant d'assez de temps libre pour l'examiner, ligne par ligne.