Claude formalise le dernier théorème de Fermat en 11 jours

Anthropic a publié le 4 septembre un communiqué détaillant cette prouesse. Son intelligence artificielle Claude a réussi à formaliser en onze jours la démonstration du dernier théorème de Fermat, c'est-à-dire à la traduire dans un langage de programmation vérifiable automatiquement par ordinateur.

Le dernier théorème de Fermat stipule que, pour tous entiers positifs a, b et c, l'équation aⁿ + bⁿ = cⁿ n'a pas de solution lorsque n est supérieur à 2. Formulé par Pierre de Fermat au XVIIe siècle, il est resté à l'état de conjecture pendant plus de trois cent cinquante ans, jusqu'à ce que le mathématicien britannique Andrew Wiles, aidé de son ancien étudiant Richard Taylor, en achève la preuve en 1994. Cette démonstration lui vaudra le prix Abel en 2016.

Une formalisation, pas une nouvelle preuve

Formaliser une démonstration mathématique consiste à la traduire dans un langage compréhensible par une machine, ici le système de preuve Lean. Contrairement à un exposé destiné à des mathématiciens, rien n'est évident pour un ordinateur : il faut reconstruire chaque définition, chaque théorème intermédiaire, chaque étape logique. Si le code final compile, la preuve est validée sans intervention d'un arbitre humain.

Claude n'a donc pas découvert de nouvelles mathématiques. Il a traduit en Lean l'argument déjà établi par Wiles et Taylor, en s'appuyant sur une exposition simplifiée due à Henri Darmon, Fred Diamond et Richard Taylor, selon Techtimes. Le mathématicien Kevin Buzzard, de l'Imperial College de Londres, qui menait depuis 2024 un projet communautaire de formalisation du même théorème, a examiné le résultat d'Anthropic. Cette prouesse fait écho à l'annonce d'OpenAI sur Navier-Stokes, présentée quatre jours plus tard.

« This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics. », Kevin Buzzard, mathématicien à l'Imperial College de Londres.

Un chantier titanesque en chiffres

Le projet, mené selon Generation-NT par le chercheur Tianyi Peng, a mobilisé plusieurs dizaines d'agents Claude travaillant de façon largement autonome entre le 7 et le 17 août 2026, avant la publication du résultat le 4 septembre. Anthropic n'intervenait qu'occasionnellement pour orienter les priorités des agents.

Ce volume de code équivaut à plus de cinq fois la taille de Mathlib, la bibliothèque communautaire de mathématiques formalisées sur laquelle s'appuie la preuve, selon Newscientist. Le résultat a été vérifié par Lean à partir de ses trois axiomes standards, sans extension extérieure, précise Anthropic.

Réactions et limites de l'exploit

Le processus n'a pas été linéaire. Anthropic reconnaît dans son document explicatif que les agents ont parfois perdu le fil du projet.

« les agents [auraient] perdu le fil de l'avancement du projet et cessé de collaborer efficacement », Anthropic, entreprise conceptrice de Claude.

Interrogée par Le Monde sur la genèse du projet et sur la concurrence que ce type d'exploit fait peser sur le travail des mathématiciens, l'entreprise n'a pas répondu. Le magazine Forbes souligne de son côté que la découverte mathématique en elle-même devient presque gratuite pour l'IA, mais que la vérification rigoureuse reste coûteuse : les six milliards de tokens de sortie consommés par Claude, facturés selon le tarif public d'Anthropic de 50 dollars par million de tokens, représentent l'équivalent d'environ un tiers de la subvention de cinq ans accordée au projet de Kevin Buzzard, dépensée en onze jours seulement.

L'hebdomadaire britannique New Scientist, cité par Courrier International, résume l'événement comme la confirmation, par des agents d'IA, qu'une preuve humaine établie dans les années 1990 était correcte, et non la découverte d'une preuve inédite. Ce scepticisme rejoint la position du mathématicien Stéphane Mallat sur les démonstrations produites par IA, et celle de vingt-cinq médaillés Fields critiques envers l'IA d'entreprise.