Treize millions de lignes de code pour une seule démonstration. C’est ce qu’a produit un modèle d’Anthropic en onze jours, pour traduire la preuve du dernier théorème de Fermat dans un langage que la machine peut contrôler pas à pas. L’exploit technique est réel. Ce qu’il garantit exactement l’est un peu moins que ce que le chiffre laisse croire.
13 millions de lignes, 29 500 théorèmes
Treize millions de lignes. C’est le volume qu’occupe, une fois traduite en langage informatique, la démonstration du dernier théorème de Fermat, cet énoncé formulé au XVIIe siècle et resté sans preuve pendant plus de trois cents ans, jusqu’à ce qu’Andrew Wiles le démontre dans les années 1990. Le 4 septembre 2026, la publication d’Anthropic a détaillé, non pas une nouvelle démonstration du théorème de Fermat, mais la formalisation complète de celle de Wiles. C’est-à-dire la réécriture de sa preuve dans un langage que l’ordinateur peut vérifier ligne par ligne, sans se fier à l’intuition humaine.
Le texte a été écrit en Lean, un langage informatique conçu pour écrire et vérifier des démonstrations mathématiques. Il démontre au passage 29 500 théorèmes intermédiaires, sur 30 300 produits au total, chacun nécessaire à l’édifice final. Pour donner une échelle : cette formalisation dépasse cinq fois la taille de Mathlib, la bibliothèque de référence des mathématiques déjà formalisées en Lean, construite par la communauté depuis des années.
Onze jours de travail. Anthropic résume la durée par « a little under two weeks » (un peu moins de deux semaines). Le chantier a consommé environ six milliards de jetons de sortie, les unités de texte qu’un modèle produit, l’équivalent approximatif de fragments de mots. Le modèle utilisé n’est pas accessible au public : Anthropic le décrit comme un « general-purpose internal research model roughly comparable to Claude Fable 5.1 » (un modèle de recherche interne généraliste, à peu près comparable à Claude Fable 5.1). L’entreprise, dont nous avions suivi le bras de fer avec le Pentagone, garde donc ses meilleurs outils pour elle.
Ce que la machine garantit, et ce qu’elle ne garantit pas
Lean vérifie une chose précise. Chaque ligne de la preuve, chaque pas logique, respecte les règles du système. Rien ne cloche entre le début et la fin du raisonnement. Il n’y a pas de trou, pas de « on admet que » caché dans les 13 millions de lignes.
Cette garantie repose sur trois axiomes seulement. Un axiome est un énoncé admis sans démonstration, sur lequel tout le reste s’appuie. Moins un système en utilise, plus il est solide. La preuve du théorème de Fermat produite par les agents n’en mobilise aucun de plus que ceux de Lean.
Vérifier qu’un raisonnement est correct ne dit pourtant rien sur ce qu’il démontre. Une preuve parfaitement valide peut porter sur un énoncé légèrement différent de celui qu’on croit prouver. C’est pour cela qu’un comparateur automatique a confronté l’énoncé final à sa version de référence dans Mathlib. Les deux correspondent. Cette étape distingue le travail d’une simple production de texte convaincant : elle relie la preuve au problème réel, pas à une reformulation approximative. La question de la vérifiabilité s’était déjà posée en août, quand OpenAI Astra a fait tomber dix problèmes de maths que tout le monde pouvait contrôler.
Le chantier n’a pas avancé en ligne droite. Des dizaines d’agents ont travaillé en parallèle pendant onze jours, coordonnés via Prove2Me, une plateforme collaborative ouverte construite par Tianyi Peng et ses collaborateurs à l’université Columbia. Elle maintient un graphe des énoncés à démontrer, ce qui permet à chaque agent de choisir quelle sous-partie attaquer ensuite, et de retrouver un résultat déjà démontré à partir d’une description en langage courant. Beaucoup de tentatives ont échoué. Anthropic écrit que « failed efforts contributed ~7% of the non-boilerplate lines in the final proof » (les tentatives infructueuses ont fourni environ 7 % des lignes utiles de la preuve finale). Ces échecs n’ont donc pas été perdus.
Une limite demeure, qu’Anthropic assume elle-même. L’entreprise écrit que sa preuve est « likely much longer than it needs to be » (probablement bien plus longue qu’elle n’aurait besoin de l’être). Mathlib doit sa concision à une relecture humaine attentive, ligne par ligne. Personne n’a lu les 13 millions de lignes produites par les agents. La compilation, l’étape où la machine relit tout le code pour vérifier qu’il tient debout, a validé la structure. Aucun humain n’a validé la forme.
0 Commentaires
Aucun commentaire pour le moment. Soyez le premier à commenter !