Fermat formalisé dans Lean : une preuve connue, désormais vérifiable par ordinateur

Un monument mathématique passé au crible d’un assistant de preuve

Le 4 septembre 2026, Anthropic a annoncé que des agents fondés sur Claude avaient produit, après environ onze jours d’exécution en grande partie autonome, ce que l’entreprise présente comme la première formalisation complète et vérifiée par ordinateur du dernier théorème de Fermat dans Lean 4. La formulation prudente est essentielle : il ne s’agit ni d’une nouvelle démonstration d’un problème encore ouvert, ni d’un résultat mathématique qui dépasserait celui obtenu dans les années 1990. Le travail consiste à rendre une démonstration connue intégralement contrôlable par un logiciel de preuve.

L’énoncé publié porte sur des entiers naturels : pour tout exposant n supérieur ou égal à 3 et tous entiers naturels strictement positifs a, b et c, l’égalité a^n + b^n = c^n est impossible. Le dépôt d’Anthropic indique que l’argument suit la voie tracée par Frey, Serre, Ribet, Wiles et Taylor–Wiles, dans la présentation classique de Darmon, Diamond et Taylor. Cette filiation donne la juste mesure de l’annonce : les agents n’ont pas découvert un raccourci inédit vers Fermat, mais ont encodé et relié une construction mathématique élaborée par des humains pendant des décennies.

Cette différence n’amoindrit pas l’intérêt du résultat. Une démonstration sur papier s’adresse à des spécialistes qui savent reconstruire les étapes omises, reconnaître les usages implicites d’un lemme et combler des détails réputés routiniers. Lean exige au contraire que chaque passage soit exprimé dans un langage formel et accepté par son noyau de vérification. Formaliser une preuve de cette ampleur revient donc à transformer une architecture mathématique considérable en une chaîne d’objets dont les dépendances peuvent être contrôlées mécaniquement.

Une échelle qui change la nature du travail

Les chiffres communiqués par Anthropic donnent une idée du chantier : 13 millions de lignes de Lean, environ six milliards de jetons produits et 30 300 résultats intermédiaires démontrés, dont près de 29 500 interviennent dans la preuve finale. Le dépôt fournit un autre inventaire, établi selon des catégories différentes : 29 511 pages consacrées aux théorèmes, 1 450 modules de définitions et 60 475 modules produits lors de la construction. Ces nombres ne doivent pas être fusionnés comme s’ils comptaient la même chose ; ils décrivent plusieurs niveaux de l’artefact.

Ils ne permettent pas non plus d’évaluer à eux seuls le coût financier ou énergétique de l’expérience. Aucun bilan public complet de ce type n’accompagne les éléments disponibles. Le volume de jetons mesure une activité de génération, pas une facture universelle : celle-ci dépendrait notamment de l’infrastructure, du matériel, des reprises et des conditions exactes d’exécution.

L’apport le plus concret se trouve ailleurs. Le résultat est publié sous la forme d’un dépôt que d’autres équipes peuvent examiner, reconstruire et soumettre aux mêmes contrôles. L’environnement est précisément fixé à Lean 4.33.1 et Mathlib v4.33.0. Ce gel des versions compte : dans un projet aussi vaste, une modification de bibliothèque ou du langage peut changer les dépendances, révéler une incompatibilité ou exiger une adaptation. Indiquer les versions transforme une annonce générale en objet technique identifiable.

Ce que la machine vérifie — et ce qu’elle ne garantit pas

Le contrôle par défaut va jusqu’à examiner les fondations logiques mobilisées par le théorème final. Celui-ci doit dépendre exactement de propext, Classical.choice et Quot.sound. Pour le lecteur non spécialiste, l’enjeu n’est pas le nom de ces trois principes, mais la traçabilité : les hypothèses admises au niveau logique sont déclarées et le vérificateur peut refuser un résultat dont la chaîne de dépendances ne correspond pas au cadre prévu.

Cette garantie reste circonscrite. Lean vérifie que le terme construit respecte ses règles et les définitions de la bibliothèque employée. Il ne certifie pas que le code est élégant, facile à entretenir ou pédagogiquement satisfaisant. Il ne transforme pas davantage l’énoncé en découverte nouvelle. Ici, la valeur tient à la formalisation complète d’une voie de preuve établie, à son contrôle informatique et à la possibilité d’en inspecter la réalisation.

Il faut également distinguer autonomie opérationnelle et indépendance intellectuelle. Anthropic décrit une exécution largement autonome pendant environ onze jours, mais l’artefact s’appuie sur les mathématiques antérieures et sur le travail humain accumulé dans les bibliothèques formelles. Les agents interviennent dans un environnement déjà riche en définitions, théorèmes et outils. Présenter cette expérience comme un remplacement soudain des mathématiciens ferait disparaître précisément ce qui l’a rendue possible.

Pourquoi ce résultat peut être utile au-delà de Fermat

L’intérêt immédiat est méthodologique. La formalisation de résultats profonds est depuis longtemps freinée par la quantité de détails qu’il faut expliciter avant même d’atteindre les passages les plus créatifs. Un système capable de produire puis de faire contrôler une masse aussi importante de code suggère une nouvelle répartition du travail : l’automatisation peut prendre en charge une partie de l’explicitation, tandis que les chercheurs concentrent leur examen sur le choix des définitions, la structure de l’argument et les endroits où une erreur conceptuelle pourrait se cacher.

Le dépôt public permet de soumettre le résultat à un examen technique contradictoire. Il ne faut pas croire l’annonce sur la seule foi d’une démonstration filmée ou d’un chiffre impressionnant : les fichiers, leurs versions et le théorème final constituent des éléments que la communauté peut confronter aux affirmations de l’entreprise. Une reconstruction réussie confirme que Lean accepte l’artefact dans l’environnement indiqué ; une difficulté de reproduction, une dépendance mal comprise ou une faiblesse de présentation peut au contraire être signalée précisément. Cette forme d’examen est plus utile qu’un débat abstrait sur les capacités générales de l’intelligence artificielle.

À plus long terme, le bénéfice dépendra de la qualité d’usage de cette base. Treize millions de lignes ne deviennent pas automatiquement une bibliothèque claire et réutilisable. Les spécialistes devront encore déterminer quelles parties sont bien structurées, lesquelles méritent d’être simplifiées et comment les résultats intermédiaires peuvent servir à d’autres développements. La taille de l’artefact est donc à la fois une prouesse et une question ouverte d’ingénierie documentaire.

La bonne nouvelle est mesurable sans être triomphaliste : un raisonnement mathématique majeur, déjà connu mais extraordinairement vaste, a été converti en un objet qu’un noyau de preuve peut contrôler de bout en bout dans un environnement versionné. Si l’examen indépendant confirme durablement sa robustesse et si ses composants deviennent exploitables, cette réalisation pourra accélérer la constitution de bibliothèques de mathématiques vérifiées. Elle ne clôt pas le travail ; elle fournit un terrain concret sur lequel le poursuivre.