Comment fonctionne Lean, le programme qui ne se fie pas à celui qui démontre

Le 4 septembre, Anthropic a publié la première démonstration complète du dernier théorème de Fermat vérifiée par ordinateur. Le théorème affirme qu’il n’existe pas d’entiers strictement positifs a, b et c tels que aⁿ + bⁿ = cⁿ lorsque n est supérieur à 2. Fermat l’a noté vers 1637 dans la marge d’un livre, et Andrew Wiles a publié la première démonstration correcte en 1995, après plus de 350 ans de tentatives infructueuses.

Anthropic n’a pas trouvé de nouvelle démonstration. Elle a réécrit celle de Wiles, dans la version exposée par Darmon, Diamond et Taylor, dans un langage appelé Lean. Le travail a été mené par des dizaines d’agents Claude pendant 11 jours, avec des indications humaines ponctuelles. Le résultat occupe 13 millions de lignes : plus de cinq fois la taille de Mathlib, la grande bibliothèque de mathématiques vérifiées que maintient la communauté.

Personne ne lira 13 millions de lignes. Pourtant, Kevin Buzzard, le mathématicien de l’Imperial College de Londres qui dirige depuis 2024 le projet communautaire de formalisation de cette même démonstration, l’a examinée et a conclu qu’elle prouve le théorème sans rien supposer d’autre que les axiomes des mathématiques.

Cinq jours plus tard, l’entreprise de sécurité Trail of Bits a publié une autre « démonstration » de Fermat. Celle-ci tenait sur un écran, et Lean la marquait elle aussi comme correcte.

Les deux faits sont vrais, et comprendre pourquoi, c’est comprendre comment fonctionne Lean. Dans l’article sur les 722 démonstrations d’OpenAI, nous avons distingué les niveaux de ce que signifie, pour un résultat, être « vérifié ». Ici, nous regardons à l’intérieur du premier : ce que fait exactement le programme, ce qu’il faut croire sur parole et ce qui s’est passé cette année quand cette partie a failli.

Une démonstration qui compile

Lean est à la fois un langage de programmation et un assistant de preuve : un programme dans lequel on écrit une démonstration avec un tel niveau de détail que l’ordinateur peut en contrôler chaque étape. Leonardo de Moura l’a lancé chez Microsoft Research en 2013, et depuis 2023 il est développé par Lean FRO, une organisation à but non lucratif créée à cette fin.

La façon la plus rapide de comprendre ce qu’il fait est de lui soumettre deux affirmations simples, l’une vraie et l’autre fausse :

example : 2 + 2 = 4 := rfl

example : 2 + 2 = 5 := rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

L’erreur dit type mismatch, une incompatibilité de types : la même erreur que donne un compilateur quand on passe un texte là où un nombre était attendu. Ce n’est pas une coïncidence de vocabulaire. Dans Lean, une affirmation est un type et une démonstration est une valeur de ce type. Vérifier une démonstration consiste à vérifier que la valeur a le bon type, de même qu’un compilateur vérifie qu’une fonction renvoie ce qu’elle prétend renvoyer.

Cette équivalence entre démonstrations et programmes est connue sous le nom de « propositions comme types » ou correspondance de Curry-Howard. Les logiciens l’ont mise au jour progressivement entre les années trente et soixante du siècle dernier, et elle est à la base de Lean et d’autres assistants comme Rocq ou Agda. Pour qui programme, la conséquence est facile à imaginer : qu’une démonstration soit correcte signifie qu’elle compile.

Écrire une démonstration, c’est dialoguer avec Lean

Presque personne n’écrit ces valeurs à la main. On utilise d’ordinaire des tactiques : des ordres comme « fais une récurrence » ou « réécris en utilisant cette égalité », qui transforment peu à peu ce qui reste à démontrer. À chaque étape, Lean affiche l’état de la démonstration : les données dont on dispose et l’objectif restant, marqué par le symbole ⊢.

Un exemple complet : démontrer qu’ajouter zéro à gauche laisse un entier naturel inchangé. Cela paraît évident, mais dans Lean ça ne l’est pas. L’addition est définie en parcourant le second nombre, si bien que n + 0 = n découle directement de la définition, alors que 0 + n = n doit être démontré.

theorem cero_mas (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [← Nat.add_assoc, ih]

n : Nat
⊢ 0 + n = n

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

⊢ 0 + k + 1 = k + 1

Le plus intéressant est ce qui se passe quand une étape échoue. Si l’on saute le regroupement et que l’on écrit directement rw [ih], Lean ne se contente pas de dire non :

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 + k
in the target expression
  0 + (k + 1) = k + 1

Il dit ce qu’il cherchait, où il le cherchait et dans quel état il est resté. Ce dialogue, où chaque étape reçoit une réponse immédiate et précise, explique en bonne partie pourquoi Lean est devenu l’un des environnements les plus utilisés par les systèmes d’IA qui font des mathématiques. Nous y reviendrons.

Sous les tactiques, un programme

Les tactiques ne sont pas la démonstration : ce sont des programmes qui la construisent. Si l’on demande à Lean d’afficher ce qu’il a enregistré sous le nom cero_mas, voici ce qui apparaît :

theorem cero_mas : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Eq.symm (Nat.add_assoc 0 k 1))))
        (Eq.mpr (id (congrArg (fun _a => _a + 1 = k + 1) ih)) (Eq.refl (k + 1))))
    n

C’est une fonction qui, pour chaque n, construit la preuve par récursion en enchaînant des égalités. Personne ne l’écrit ainsi ; ce sont les tactiques qui la génèrent. Et c’est cet objet, appelé terme de preuve, qui est vérifié.

Cette séparation est la décision de conception la plus importante de Lean. Les tactiques peuvent être aussi sophistiquées qu’on le souhaite. Certaines résolvent seules des problèmes d’arithmétique, comme omega, ou cherchent des combinaisons de faits connus, comme grind, et chacun peut écrire les siennes. Aucune n’a besoin d’être correcte. Tout ce qu’elles produisent finit converti en un terme comme celui ci-dessus, et ce terme est contrôlé par un petit composant appelé noyau (kernel, en anglais), qui ne connaît que les règles de base de la logique de Lean. Si une tactique comporte une erreur et construit quelque chose d’invalide, le noyau le rejette. Le guide officiel pour valider une démonstration range les erreurs des tactiques parmi ce qui est déjà couvert par la simple compilation.

L’idée qu’une grosse machinerie produise des résultats et qu’un petit vérificateur les contrôle est connue sous le nom de critère de De Bruijn, d’après le mathématicien néerlandais qui l’a mise en pratique dans son système Automath à la fin des années soixante.

Cette séparation est décisive pour l’intelligence artificielle. Pour Lean, un modèle de langage n’est qu’une tactique de plus : quelque chose qui propose des étapes. Il peut inventer un lemme, prendre un chemin absurde ou générer treize millions de lignes. Lean n’a pas besoin de s’y fier, pas plus qu’il ne se fie à la personne qui écrit ou à omega.

Trois axiomes et un sorry

Que le noyau accepte quelque chose ne suffit pas pour savoir ce qui a été démontré. Lean permet de travailler avec des trous et avec des suppositions, et les uns comme les autres passent facilement inaperçus.

Le trou s’appelle sorry : un mot que l’on écrit à la place d’une démonstration en attente. Lean l’accepte pour qu’on puisse avancer par morceaux, mais il prévient et en garde la trace. Les suppositions sont les axiomes, des affirmations admises sans démonstration. Lean en fournit trois d’origine, que la pratique mathématique habituelle tient pour acquis malgré leurs noms peu engageants :

• propext : deux affirmations qui s’impliquent l’une l’autre sont la même affirmation.
• Quot.sound : on peut traiter comme un seul objet tous ceux que l’on considère équivalents. C’est l’opération qui permet de construire, par exemple, les fractions à partir de couples d’entiers, où 1/2 et 2/4 sont le même nombre.
• Classical.choice : dans un ensemble non vide, on peut choisir un élément, même sans savoir lequel. C’est l’axiome du choix.

Mais n’importe qui peut en ajouter d’autres, y compris des axiomes faux. C’est pourquoi la commande la plus importante pour examiner la démonstration d’autrui n’est pas de la compiler, mais de demander à Lean de quoi elle dépend, avec #print axioms. Avec nos exemples :

theorem trampa : 2 + 2 = 5 := by sorry

theorem cero_mas' (n : Nat) : 0 + n = n := by
  omega

'cero_mas' does not depend on any axioms
'cero_mas'' depends on axioms: [propext, Quot.sound]
'trampa' depends on axioms: [sorryAx]

Le guide de la communauté pour savoir si quelque chose est démontré demande exactement cela : que la réponse ne comprenne rien en dehors de ces trois axiomes. Le dépôt de Fermat en fait une condition de compilation :

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

La « démonstration » qui tenait dans la marge

On comprend maintenant l’astuce de Trail of Bits. Sa démonstration utilisait native_decide, une tactique qui, pour aller plus vite, ne laisse pas le noyau effectuer un calcul, mais l’exécute sous forme de code compilé. C’est utile pour les gros calculs, mais cela a un prix : en plus du noyau, il faut faire confiance au compilateur. Lean l’enregistre en ajoutant un axiome à la liste.

Le code compilé d’une fonction contenait une erreur. La fonction qui extrait un morceau d’un texte donnait des résultats différents selon que l’on raisonnait sur elle ou qu’on l’exécutait. Si l’on demandait un fragment à partir d’une position astronomiquement grande, sa définition logique renvoyait un texte vide, tandis que le code compilé renvoyait le texte entier. Trail of Bits a utilisé les deux réponses pour conclure qu’un texte vide était égal à un texte qui ne l’était pas. Et d’une contradiction, on peut déduire n’importe quoi, y compris le théorème de Fermat.

L’éditeur affichait les marques bleues de « correct ». Mais #print axioms ajoutait aux trois standard un axiome de plus : flt._native.native_decide.ax_1_1. Trail of Bits a elle-même précisé qu’il ne s’agissait pas d’une faille du noyau. L’équipe de Lean a corrigé la partie la plus grave en trois heures environ et le reste, cinq jours plus tard. L’erreur touchait toutes les versions stables jusqu’à la 4.33.1, précisément celle qu’utilise le dépôt de Fermat d’Anthropic. Ce projet n’est pas concerné : il interdit native_decide et exige exactement les trois axiomes.

La leçon est pratique. Le verdict n’est pas la marque bleue de l’éditeur, mais la liste des axiomes. Le guide officiel le dit expressément : les marques bleues apparaissent même si l’une des pièces sur lesquelles s’appuie le théorème utilise sorry, et un axiome qui contient _native dans son nom indique qu’une partie du calcul a été faite par du code compilé.

Et si c’est le noyau qui se trompe ?

Le noyau est petit, mais pas infaillible, et on l’a vu en juillet.

Le 25 juillet, Ramana Kumar a publié une réfutation de la conjecture de Collatz obtenue avec l’aide de l’IA. La conjecture affirme que, si l’on prend n’importe quel entier strictement positif et qu’on le divise par deux quand il est pair, ou qu’on le multiplie par trois et qu’on lui ajoute un quand il est impair, on finit tôt ou tard par arriver à 1. La réfutation ne contenait aucun sorry. Elle n’était pas valide pour autant : elle exploitait une erreur du noyau dans le traitement des types inductifs imbriqués, c’est-à-dire des types définis en fonction d’eux-mêmes à l’intérieur d’autres types, comme un arbre dont les branches sont une liste d’arbres.

Le 28 juillet, Kiran Gopinathan l’a réduite à une démonstration de « faux » et l’a signalée. Une heure plus tard, une correction existait, publiée dans Lean 4.32.2. La démonstration de Fermat a été compilée avec la 4.33.1, qui l’inclut déjà. D’après l’analyse publiée ensuite par Leonardo de Moura, la faille n’était atteignable que par métaprogrammation, c’est-à-dire avec des programmes qui envoient des déclarations directement au noyau sans passer par les contrôles habituels.

L’aspect le plus instructif est la seconde vérification. Comme le noyau peut se tromper, il existe des noyaux indépendants : des programmes écrits de zéro qui revérifient les mêmes termes. Le principal est nanoda, écrit en Rust par Chris Bailey. La réfutation de Kumar avait aussi passé une version de nanoda vieille d’une semaine, parce qu’elle exploitait en même temps une autre erreur de nanoda, différente et déjà corrigée. Il a fallu deux erreurs sans rapport dans deux implémentations à la fois. La conclusion de De Moura est que la vérification indépendante continue de fonctionner, à condition d’utiliser des versions à jour des deux. Par la suite, un chercheur d’OpenAI, aidé d’une IA spécialisée en sécurité, a trouvé d’autres erreurs dans le noyau, toutes atteignables uniquement par métaprogrammation. Le vérificateur nanoda les a toutes détectées.

Lean FRO soumettait déjà publiquement les vérificateurs indépendants à l’épreuve dans la Lean Kernel Arena, et après juillet, l’organisation y a ajouté les tests de ces erreurs et s’est engagée à investir dans davantage d’implémentations. Le vérificateur le plus frappant est con-leche, publié en septembre : un vérificateur externe accompagné d’une démonstration, écrite en Lean, qu’il n’accepte jamais une preuve de « faux ». Son README raconte qu’il a été implémenté et démontré par Claude, sous la supervision de Joachim Breitner, de Lean FRO, qui décrit le code comme un tas désordonné qui fonctionne et qui est démontré. Il n’élimine pas toute circularité, car cette démonstration est à son tour vérifiée par un noyau de Lean, mais une erreur devrait se glisser dans des pièces qui fonctionnent différemment.

Le guide officiel de Lean classe toutes ces vérifications de la moins exigeante à la plus exigeante. Chaque niveau ajoute une protection, mais laisse aussi quelque chose de côté :

Source : « Validating a Lean Proof », manuel de référence de Lean. Synthèse de Codin. Le guide réserve le dernier niveau aux situations à haut risque, comme les compétitions dotées de prix ou les systèmes d’IA dont on ne peut pas tenir pour acquis qu’ils agissent de bonne foi.

La démonstration de Fermat d’Anthropic est passée par le dernier : le noyau officiel, une version de nanoda qui a examiné 1 052 234 déclarations sans erreur et Comparator, l’outil qui vérifie dans un environnement isolé que l’énoncé démontré est identique à celui de référence. Ce n’est pas une certitude absolue. C’est autre chose : faire confiance à quelque chose de petit, de public et vérifié de plusieurs façons.

Ce qu’aucun programme ne vérifie

Le noyau garantit que le terme démontre l’énoncé écrit. Il ne garantit pas que cet énoncé dise ce que nous croyons. Le guide de la communauté donne des exemples : on peut redéfinir ce que sont les entiers naturels, ou appeler TheRiemannHypothesis n’importe quelle affirmation, et démontrer quelque chose qui ressemble à un grand théorème sans en être un.

L’énoncé de Fermat est écrit avec les entiers naturels et les opérations que fournit Lean. Seule la puissance vient de Mathlib, et Comparator vérifie qu’elle coïncide avec l’énoncé que Mathlib avait déjà, relu par ses responsables. C’est pourquoi il est facile de lui faire confiance. Ce qu’aucun outil ne peut vérifier, prévient le dépôt lui-même, c’est que chacun des 29 511 théorèmes intermédiaires signifie ce que suggère son nom. Pour le résultat final, peu importe, car le noyau vérifie tout ce qui se trouve en dessous. Pour qu’une personne apprenne quelque chose de cette démonstration, si.

C’est là qu’intervient la fonction la moins visible de Mathlib. Au 8 octobre 2026, elle réunit 290 229 théorèmes et 137 964 définitions de 772 personnes. Sa valeur ne tient pas seulement à la quantité : ce sont des définitions partagées et relues, sur lesquelles on peut lire un nouvel énoncé sans se méfier de chaque mot. Quand un résultat a besoin de définitions que Mathlib ne contient pas, quelqu’un du domaine doit les relire, comme nous l’avons expliqué à propos des cas d’OpenAI qui s’appuyaient sur des définitions propres.

Pourquoi Lean convient si bien à l’IA

Revenons au dialogue du début. Lean répond à chaque étape avec précision, et son verdict final est un oui ou un non qu’on ne peut pas contester en ayant l’air convaincant. Pour un système d’IA, c’est un entraîneur idéal. Dans notre tour d’horizon de ce qui a fait progresser les modèles de langage, nous avons expliqué comment l’entraînement avec des récompenses vérifiables a changé leur façon de raisonner. Lean pousse cette idée à l’extrême.

AlphaProof, de Google DeepMind, est l’exemple le mieux documenté. Selon son article dans Nature, publié en novembre 2025, il a appris à chercher des démonstrations en Lean par apprentissage par renforcement, avec une méthode inspirée d’AlphaZero et des millions de problèmes traduits automatiquement en Lean. Avec AlphaGeometry 2, il a obtenu aux Olympiades internationales de mathématiques de 2024 un score équivalent à une médaille d’argent. Anthropic raconte quelque chose de semblable dans une autre direction : Claude utilise des démonstrations partielles en Lean pour vérifier ses propres hypothèses pendant qu’il travaille, comme il utiliserait une simulation numérique pour voir s’il est sur la bonne voie.

Cette même rigueur a une conséquence gênante. Un système optimisé pour que Lean dise oui trouvera les failles de Lean s’il y en a. La réfutation de Collatz a été obtenue avec l’aide de l’IA. Joachim Breitner a fait remarquer que ce n’était peut-être pas un hasard si les deux erreurs étaient apparues presque en même temps : il existe déjà des modèles capables de les trouver. Le guide officiel de Lean range d’ailleurs les démonstrations générées par IA et non relues dans le même groupe que celles qui cherchent délibérément à tromper. Plus les systèmes qui génèrent sont performants, plus il importe que le vérificateur soit petit, relu et redondant.

Vérifier n’est pas gratuit non plus. La démonstration de Fermat a coûté environ 6 milliards de tokens de sortie et plusieurs tentatives infructueuses avant qu’une plateforme de coordination, Prove2Me, maintienne en ordre le travail des agents. Refaire la vérification coûte bien moins cher que relire la démonstration à la main, mais ce n’est pas anodin : selon le dépôt, la compiler a pris cinq heures et demie avec 96 processus en parallèle, et Comparator, près de quinze heures avec des pics de 230 Go de mémoire.

La même répartition, hors des mathématiques

Ce que Lean organise pour les mathématiques sert déjà pour du logiciel en production.

Chez AWS, l’équipe de Cedar, le langage dans lequel on écrit les politiques d’autorisation (qui peut faire quoi sur quelle ressource), maintient un modèle de chaque composant en Lean, environ dix fois plus petit que le code réel en Rust. Elle démontre des propriétés de sécurité sur ce modèle et génère des millions d’entrées aléatoires pour vérifier que le modèle et le code répondent la même chose. D’après le cas publié par Lean, aucune nouvelle version de Cedar ne sort si le modèle, les démonstrations et ces tests ne sont pas à jour.

Chez Microsoft, SymCrypt, la bibliothèque cryptographique qu’utilisent Windows et Azure, écrit ses nouveaux algorithmes en Rust, les traduit en Lean avec un outil appelé Aeneas et démontre qu’ils respectent des spécifications dérivées des normes du NIST. En juillet, l’équipe a publié les premières démonstrations complètes : ML-KEM, un algorithme d’échange de clés résistant aux ordinateurs quantiques, et SHA-3. Le schéma qu’ils utilisent pour l’expliquer répartit le travail en trois. Les agents d’IA, qu’ils qualifient de stochastiques, écrivent les démonstrations. Les outils, déterministes, compilent, traduisent et vérifient. Et les personnes consacrent leur attention à examiner comment les normes ont été formalisées et quelles propriétés comptent.

Cette répartition est ce que Lean a de plus transposable pour toute équipe qui intègre l’IA dans un processus, même si elle n’écrira jamais une démonstration. La génération peut être abondante et peu fiable si trois conditions sont réunies. Ce qui vérifie est petit, déterministe et indépendant de ce qui génère. On sait exactement ce qui a été tenu pour acquis, l’équivalent de #print axioms : quels tests ont été sautés, ce qui a été simulé, ce qui a été accepté sans relecture. Et les personnes relisent la spécification, la partie qu’aucune machine ne peut valider à leur place. Les tests et les systèmes de types sont des versions faibles de la même idée ; Lean en est la version extrême.

Lean ne se fie pas à celui qui démontre, qu’il s’agisse d’une personne, d’une tactique ou d’un modèle. Nous, en revanche, devons bien nous fier à quelque chose. Ce qui a changé, c’est sa taille : ce n’est plus la réputation d’un auteur ni des années de relecture, mais un petit noyau, trois axiomes et un énoncé qui tient en deux lignes. La question utile n’est plus de savoir à quel point nous faisons confiance au modèle, mais quel est le minimum que nous devons croire sur parole et qui l’a vérifié.

Sources

• Anthropic : « Formalizing Fermat’s Last Theorem », 4 septembre 2026 et dépôt anthropics/fermats-last-theorem, consulté le 8 octobre 2026.
• Trail of Bits : « A “proof” of Fermat’s Last Theorem that fits the margin », 9 septembre 2026.
• Leonardo de Moura : analyse de la faille du noyau #14576, 1er août 2026 et notes de version de Lean 4.32.2, 28 juillet 2026.
• con-leche : vérificateur externe de Lean avec démonstration de cohérence et Lean Kernel Arena.
• Communauté Lean : « Did you prove it? » et statistiques de Mathlib, consultées le 8 octobre 2026.
• Lean FRO : histoire et organisation et manuel de référence de Lean : « Validating a Lean Proof ».
• Hubert et al. : « Olympiad-level formal mathematical reasoning with reinforcement learning », Nature, novembre 2025.
• Lean : cas de Cedar chez AWS et AWS Open Source Blog : « Lean into verified software development ».
• Microsoft Research : « Verifying Rust cryptography in SymCrypt, from standards to code », 13 juillet 2026.
• Nos propres exemples de code ont été testés dans l’éditeur web officiel de Lean avec la version v4.35.0-rc4.