Contexte et objectifs
Le dernier théorème de Fermat (FLT) a été démontré pour la première fois en 1995 par Andrew Wiles, une preuve de 129 pages nécessitant plusieurs années de vérification humaine. Depuis 2024, la communauté mathématique, menée par Kevin Buzzard, travaille à transposer cette démonstration dans le système de preuve assistée Lean, afin de rendre chaque étape vérifiable par ordinateur. L’objectif déclaré était de produire une formalisation complète en plusieurs années, le plan initial s’étalant sur 86 pages de spécifications.
Anthropic a testé la capacité de son modèle Claude à accélérer ce processus. En 11 jours, Claude a généré une preuve entièrement vérifiée, incluant 29 500 théorèmes intermédiaires et totalisant 13 millions de lignes de code Lean, soit plus de cinq fois la taille actuelle de la bibliothèque Mathlib sur laquelle s’appuie la preuve.
Architecture de l'auto‑formalisation
Le workflow repose sur trois composants clés : le modèle Claude, la plateforme collaborative Prove2Me et le moteur Lean. Claude opère via un harnais multi‑agents ; chaque agent reçoit des tâches spécifiques (définition de concepts, preuve de lemmas, intégration de résultats) et communique ses avancées à travers Prove2Me. Cette plateforme assure la persistance du contexte, la synchronisation des agents et la validation incrémentale des preuves.
Les instructions humaines ont été limitées à des directives de haut niveau, par exemple « Jacobian as a scheme sounds high priority » ou « push Mazur theorem to be done soon ». Le modèle a alors traduit ces objectifs en séquences Lean, en générant automatiquement les preuves de chaque sous‑théorème. Le processus a nécessité la réécriture de chaque raisonnement, même les étapes jugées triviales, car Lean ne tolère aucune omission.
THE FLT root reads PROVED. Historic moment (modulo re-check).
!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root.
🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18Analyse des performances et limites
Le facteur de temps (11 jours) contraste fortement avec les prévisions initiales de plusieurs années. Cette accélération provient principalement de la parallélisation : les agents ont produit simultanément près de 30 300 théorèmes, dont 29 500 ont été retenus dans la version finale. Cependant, 7 % des lignes non‑boilerplate proviennent d’essais infructueux, illustrant une perte d’efficacité liée à la perte de suivi d’état des agents.
En termes de volume, 13 M lignes Lean dépassent de cinq fois la taille de Mathlib, ce qui indique une redondance importante ; la plupart des définitions sont ré‑implémentées pour satisfaire les exigences de vérifiabilité. Cette surcharge pose des défis de maintenance : chaque mise à jour de Mathlib devra être ré‑intégrée dans le projet FLT, augmentant le coût de long terme.
Sur le plan méthodologique, la preuve repose sur une version simplifiée du schéma de Wiles (Darmon‑Diamond‑Taylor). La dépendance à des constructions avancées (schémas de Jacobian, théorème de Mazur) montre que le modèle a déjà intégré des domaines variés (algèbre, analyse harmonique, géométrie). Néanmoins, l’absence de nouvelles idées mathématiques – la contribution reste la vérification – souligne que l’auto‑formalisation ne remplace pas la créativité humaine, mais allège la charge de validation.
En résumé, l’expérience démontre que les modèles de langage peuvent automatiser la traduction d’une preuve complexe en code vérifiable, tout en révélant des limites liées à la redondance de code, à la gestion d’état multi‑agents et à la dépendance à une bibliothèque de base encore incomplète.
