Lean valide la preuve Fermat de Claude

Lean a validé une formalisation complète du dernier théorème de Fermat produite par Claude. Le résultat est vérifiable, mais la campagne menée en onze jours par Anthropic ne peut être reproduite faute d’accès au modèle, à l’infrastructure et aux moyens de calcul employés.

Lean, un logiciel de vérification de preuves utilisé par les mathématiciens du monde entier, a accepté une version formelle complète du dernier théorème de Fermat. Produite par Claude, le système d’Anthropic, et publiée dans un dépôt ouvert, elle ne contient ni étape laissée en suspens, ni axiome supplémentaire, ni raccourci de calcul extérieur aux fondements standards de Lean (dépôt). Kevin Buzzard, mathématicien à l’Imperial College London qui dirigeait sa propre entreprise de formalisation, a compilé le projet séparément et confirmé sa validité, saluant « une réalisation extraordinaire en matière d’autoformalisation » (Buzzard).

Le problème mathématique, lui, était résolu depuis longtemps : Andrew Wiles a démontré le théorème en 1995, et aucun mathématicien sérieux n’en contestait la validité. Restait à traduire cette preuve en instructions assez précises pour un logiciel dépourvu d’intuition, en explicitant chaque définition et chaque étape intermédiaire que l’auteur pouvait laisser implicite. Selon Anthropic, des dizaines d’agents d’intelligence artificielle ont accompli cette tâche en onze jours au mois d’août, en travaillant parallèlement sur une plateforme appelée Prove2Me (Anthropic).

Ce délai ne décrit toutefois pas une expérience que des tiers pourraient reproduire. Anthropic n’a publié ni son modèle interne, ni son infrastructure d’orchestration, ni le détail des décisions prises par les opérateurs, ni les moyens de calcul mobilisés. Le résultat final, en revanche, est vérifiable : avec du matériel suffisamment puissant, chacun peut recompiler le projet Lean et constater que la preuve passe le contrôle. Un second vérificateur, écrit en Rust par Anthropic, a examiné le même objet formel et confirmé la cohérence de ses 1 052 234 déclarations (rapport technique). Il s’agit d’une nouvelle lecture du même texte, et non d’une reproduction indépendante de la campagne de onze jours.

Comment les agents ont travaillé

Formaliser une preuve consiste à réécrire le raisonnement d’un mathématicien pour qu’un programme sans intuition puisse en contrôler chaque articulation logique. L’énoncé paraît simple : pour tout exposant entier supérieur ou égal à trois, il n’existe pas trois entiers strictement positifs vérifiant aⁿ + bⁿ = cⁿ. Sa démonstration mobilise pourtant, sur des centaines de pages, plusieurs strates profondes de la théorie des nombres.

Claude n’a découvert aucun résultat mathématique nouveau. Le système a formalisé l’enchaînement déjà établi des résultats conduisant à la preuve de Wiles, en suivant un exposé des mathématiciens Henri Darmon, Fred Diamond et Richard Taylor (Anthropic, rapport technique). L’invention mathématique revient à Wiles et à ses prédécesseurs ; Claude a transcrit cet héritage en quelque 10,5 millions de lignes de code vérifiables par une machine (rapport technique).

Prove2Me, la plateforme conçue par Tianyi Peng, chercheur chez Anthropic, avec des collaborateurs de Columbia University, a décomposé la preuve en un graphe de dépendances comptant environ 29 511 propositions autonomes (rapport technique). Les agents choisissaient les propositions dont les prérequis étaient déjà établis, rédigeaient leur preuve dans Lean puis contrôlaient les énoncés proposés par leurs pairs. Cette organisation parallèle a consommé environ six milliards de jetons en sortie d’un modèle de recherche interne (rapport technique).

D’après Anthropic, les opérateurs humains n’ont écrit aucune ligne de code Lean pendant l’exécution. Ils ont néanmoins choisi le théorème, fourni l’itinéraire de preuve connu, conçu l’infrastructure des agents et parfois réorienté les priorités (Anthropic). L’entreprise n’a communiqué ni l’intégralité de leurs échanges avec le système, ni le coût de calcul.

Des années de travail humain en amont

Le résultat repose sur Mathlib, la vaste bibliothèque de mathématiques formalisées entretenue par une communauté, ainsi que sur deux projets antérieurs. Depuis la fin de 2023, l’équipe de Kevin Buzzard à l’Imperial travaillait à sa propre formalisation du dernier théorème de Fermat dans Lean, grâce à une subvention de 1 million de livres sterling accordée par l’EPSRC et prévue jusqu’en 2029 (financement de l’EPSRC). Un autre projet communautaire avait déjà formalisé le théorème pour une partie des cas. Le fichier d’attribution d’Anthropic recense 106 fichiers contenant des éléments repris ou adaptés de ces travaux (attribution).

Le parallélisme rend les onze jours calendaires impossibles à comparer directement avec le temps de travail humain consacré au projet de Buzzard, engagé depuis environ 22 mois financés lorsque la campagne de Claude a commencé (financement de l’EPSRC). Anthropic n’a publié ni le nombre d’heures de calcul sur processeurs graphiques, ni la consommation énergétique correspondante.

Avant cette publication, le dernier théorème de Fermat était le seul élément restant sur la liste de Freek Wiedijk, qui réunit cent théorèmes importants à formaliser et sert depuis vingt ans de référence pour mesurer les progrès du domaine (Buzzard).

La portée réelle de cette méthode se mesurera sur des mathématiques récentes et moins documentées, sans feuille de route, bibliothèque mûre ni travail préalable de formalisation. Ici, les agents se sont attaqués à un théorème célèbre en bénéficiant d’une infrastructure déjà substantielle. L’expérience établit qu’à partir d’un chemin de preuve connu et de travaux formels antérieurs, des agents d’intelligence artificielle peuvent produire une formalisation complète, acceptée par Lean et contrôlable par des tiers. Elle ne permet pas encore de reproduire la méthode qui a servi à la générer.