Anthropic a publié en open source, sous licence Apache 2.0, une preuve complète et vérifiée par machine du grand théorème de Fermat en Lean 4, construite sur la bibliothèque mathématique Mathlib. L'énoncé formel donné par le dépôt est : pour tout n ≥ 3 et tous entiers positifs a, b, c, a^n + b^n ≠ c^n. Cette phrase a été écrite en Lean sous la forme d'un théorème que le noyau peut vérifier étape par étape, sans laisser aucune faille.
L'ampleur est l'aspect le plus frappant de ce travail. Le dépôt recense 60 475 modules, 29 511 théorèmes, 1 450 modules de définitions ; la vérification à l'export a couvert 1 052 234 déclarations. La documentation HTML générée pèse environ 390 Mo, et le fichier d'export complet 37,8 Go. Pour tout exécuter en local, il faut plus de 300 Go d'espace disque et un pic de mémoire d'environ 153 Go.
Trois vérifications, toutes consignées
Le dépôt ne se contente pas d'un simple "ça compile". La première vérification est la compilation complète par le noyau de Lean 4.33.1 lui-même, effectuée en 5 heures 32 sur une machine à 96 cœurs. La deuxième utilise l'outil officiel comparator de leanprover (v4.33.0) pour recontrôler le tout, en environ 14 heures 46. La troisième passe par le noyau indépendant écrit en Rust nanoda 0.4.13, qui avec 16 threads a mis environ 30 minutes et a produit la sortie "Your solution is okay!".
Au-delà de ces trois vérifications, une contrainte stricte s'applique : aucun module ne doit contenir `axiom`, `sorry`, `native_decide`, `unsafe`, `extern`, `implemented_by`, `partial def` ni `#eval`. Ces mots-clés sont reconnus dans la communauté Lean comme des portes d'entrée pour les failles — `sorry` signifie directement "ceci n'est pas encore démontré", tandis que `native_decide` délègue une partie du jugement à du code machine non vérifié par le noyau. Les exclure tous revient à admettre que la crédibilité de cette preuve repose uniquement sur le noyau de Lean et les outils de vérification — c'est d'ailleurs ce qu'écrit le README lui-même.
La part écrite par l'IA, le dépôt ne le dit pas
Selon le README, le code source Lean a été "produit par des agents d'IA à partir de code Lean open source écrit par des humains, Lean faisant office d'arbitre". La proportion exacte n'est pas révélée : quels modules ont été écrits par des humains et lesquels ont été générés par le modèle puis rejetés par le noyau pour être refaits ne figure pas dans les documents publics.
La base humaine, elle, est assez clairement indiquée. 106 fichiers de dépendances proviennent de projets académiques déjà existants, principalement le projet de formalisation du FLT dirigé par Kevin Buzzard à l'Imperial College et flt-regular, qui traite le théorème de Kummer ; 23 autres modules redémontrent des contenus déjà présents dans Mathlib.
Replacé dans la trajectoire des mathématiques formalisées, ce saut d'échelle est assez frappant. Le théorème des quatre couleurs a été formalisé par Georges Gonthier en Coq en 2005, et le projet Flyspeck sur la conjecture de Kepler a été déclaré achevé en 2014 — les deux se comptant en personnes-année. Au lancement du projet FLT, l'équipe de Buzzard tablait elle aussi sur un horizon de plusieurs années. La mesure dans laquelle ce dépôt a avancé cette échéance dépend de la proportion réelle entre travail humain et travail machine — et c'est justement le seul chiffre qu'il est aujourd'hui impossible de vérifier.
Sources : README public et journaux de vérification d'Anthropic, CocoLoop, projet Mathlib, documents publics du projet FLT de l'Imperial College ; le nombre de modules, le nombre de théorèmes et la durée des trois vérifications ont été recoupés avec les données du dépôt.