L’intelligence artificielle Claude, conçue par Anthropic, vient de produire la première preuve entièrement vérifiée par ordinateur du théorème de Fermat. L’opération, achevée début septembre 2026 en seulement onze jours, a généré treize millions de lignes de code dans le langage de vérification Lean.
L’essentiel
- Claude a formalisé la preuve du théorème de Fermat en 11 jours, un chantier jugé jusque-là impossible à boucler avant plusieurs années
- Le résultat représente 13 millions de lignes de code vérifiées automatiquement dans le langage Lean
- Le mathématicien Kevin Buzzard, de l’Imperial College de Londres, a validé la démonstration
- La preuve originale, signée Andrew Wiles en 1995, s’appuyait sur des travaux accumulés depuis le XVIIe siècle
Ce qu’on sait
Le résultat a été confirmé par Anthropic dans un billet de recherche publié le 4 septembre 2026. L’entreprise explique avoir demandé à Claude de « formaliser » la preuve du théorème de Fermat, c’est-à-dire de la retranscrire dans un langage que des logiciels peuvent vérifier ligne par ligne, sans intervention humaine.
Le résultat impressionne par son ampleur. Claude a rédigé environ 13 millions de lignes de code Lean et démontré au passage 29 500 théorèmes intermédiaires, pour un total de 30 300 étapes logiques.
Ce succès conforte la place de Claude dans le comparatif IA des assistants conversationnels, où Anthropic revendique une avance sur le raisonnement long format face à ses concurrents.
L’IA a consommé près de 6 milliards de tokens de sortie pour venir à bout du chantier. Le mathématicien Kevin Buzzard, de l’Imperial College de Londres, a supervisé la relecture. Il a confirmé que l’énoncé final correspondait bien à la version reconnue par la communauté mathématique.
Un détail a rendu le projet possible : la plateforme collaborative Prove2Me, conçue par le chercheur Tianyi Peng à l’université Columbia. Elle a permis à plusieurs instances de Claude de travailler en parallèle sur un même arbre de dépendances, sans se marcher dessus.
Le contexte
Le théorème de Fermat énonce qu’aucune solution entière positive n’existe à l’équation xⁿ + yⁿ = zⁿ pour un exposant n strictement supérieur à 2. Formulé au XVIIe siècle, il n’a été démontré qu’en 1995 par le mathématicien britannique Andrew Wiles, après plus de sept ans de travail solitaire.
Cette démonstration originale s’appuie elle-même sur des décennies de recherches, notamment celles de Richard Taylor, Barry Mazur et Robert Langlands. Sa complexité est telle que la « formaliser », c’est-à-dire la rendre vérifiable pas à pas par un ordinateur, était jusqu’ici estimée à plusieurs années de travail humain.
C’est précisément ce à quoi sert le langage Lean, un assistant de preuve utilisé par les mathématiciens pour éliminer tout risque d’erreur ou d’approximation dans un raisonnement. Chaque étape, même la plus triviale en apparence, doit être justifiée pour que le logiciel l’accepte.
Ce travail s’inscrit dans une actualité chargée pour l’entreprise ces derniers jours : Anthropic vient d’obtenir gain de cause face au Pentagone devant la justice américaine, un dossier distinct mais qui confirme l’exposition croissante de la société.
La suite
Kevin Buzzard voit dans ce résultat une étape vers l’automatisation d’une bonne partie de la littérature mathématique moderne. Selon lui, si la formalisation du théorème de Fermat est désormais possible en quelques jours, d’autres démonstrations réputées complexes pourraient suivre le même chemin.
Anthropic reconnaît toutefois des limites. La preuve produite par Claude est nettement plus longue que nécessaire, l’IA se montrant moins concise qu’un mathématicien expérimenté. Environ 7 % du code final provient de tentatives ratées, corrigées au fil du chantier.
L’enjeu dépasse la seule prouesse technique. Une preuve vérifiée automatiquement réduit la charge de relecture par les pairs et permet de repérer plus vite d’éventuelles erreurs, un sujet sensible à l’heure où d’autres IA génératives, comme le nouveau modèle GPT-6 Astra d’OpenAI, inquiètent davantage qu’elles ne rassurent sur leur fiabilité.
Anthropic n’a pas précisé si Claude allait être mobilisé sur d’autres grandes conjectures mathématiques. Les prochaines semaines diront si ce chantier reste un exploit isolé ou le point de départ d’une nouvelle méthode de travail pour les mathématiciens.
