Un assistant de preuve capable de valider une démonstration de la conjecture de Collatz, voilà qui aurait fait l’effet d’une bombe dans le monde des mathématiques formelles. Sauf que la preuve en question, générée par une IA, exploitait un bug de sûreté bien réel dans le noyau de Lean. La communauté s’est enflammée, et Leo de Moura, créateur du système, a répondu avec un postmortem d’une transparence exemplaire.
L’affaire a secoué les utilisateurs de Lean bien au-delà des cercles académiques. Une question posée sur MathOverflow résume l’inquiétude ambiante : « Are we stuck with Lean ? » Autrement dit, peut-on encore faire confiance à un noyau qui a laissé passer une preuve de False ?
Aux origines du bug #14576 : une faille dans les types inductifs imbriqués
Tout commence le 25 juillet 2026, quand Ramana Kumar publie un dépôt contenant une « preuve » de la conjecture de Collatz, construite avec l’aide d’une intelligence artificielle. La démonstration ne contient aucun sorry, ces trous qui signalent habituellement une preuve incomplète. Pourtant, elle n’est pas valide.
Le 28 juillet, Kiran Gopinathan réduit le problème à un noyau minimal : une preuve de False tient en quelques lignes. Le bug #14576 est ouvert. Une heure plus tard, l’équipe Lean propose un correctif, revu par Joachim Breitner, puis fusionné. Des versions correctives sont déployées dans la foulée.
La faille se niche dans la gestion des types inductifs imbriqués par le noyau. Lorsque le kernel élimine une occurrence imbriquée sous un type inductif T avec des paramètres Ds, et que ces paramètres sont fantômes (absents des champs des constructeurs), ils disparaissent du type auxiliaire généré et échappent à la vérification de typage. Résultat : un terme mal typé peut être glissé à cet endroit précis, et le noyau accepte une preuve de False.
Il est important de souligner que ce bug de sûreté dans le noyau de Lean n’est exploitable que par métaprogrammation, en envoyant directement une déclaration inductive au kernel. Le frontend, lui, vérifie les arguments et bloque le terme mal typé. Leo de Moura insiste : il s’agit d’un bug d’implémentation, pas d’une faille dans la méta-théorie de Lean.
Pourquoi nanoda n’a rien vu
L’un des aspects les plus surprenants de cet incident concerne nanoda, le vérificateur externe indépendant de Lean développé en Rust par Chris Bailey. La preuve de Collatz passait aussi dans une version de nanoda vieille d’une semaine. Deux bugs distincts, donc, dans deux implémentations différentes.
Le kernel officiel omettait une vérification dans la prise en charge des types inductifs imbriqués. De son côté, nanoda vérifiait bien cet endroit précis, mais ne contrôlait pas le nom du type dans un nœud de projection. Un bug découvert par Jeremy Chen et corrigé une semaine avant le bug Lean. La preuve fautive exploitait simultanément les deux failles.
Ramana Kumar estime que la coïncidence temporelle est fortuite, sans exclure que le modèle d’IA ait eu connaissance du rapport de bug nanoda. Joachim Breitner avance une hypothèse plus large : la disponibilité récente de modèles suffisamment puissants pour débusquer ce type de faille expliquerait cette synchronisation troublante.
La conséquence pratique est rassurante : vérifier avec un kernel indépendant fonctionne toujours, puisqu’il a fallu deux bugs distincts dans deux implémentations. Mais les utilisateurs qui s’appuient sur cette double vérification doivent impérativement garder leurs deux outils à jour.
Métaprogrammation : supprimer l’accès n’est pas la solution
Dans les discussions qui ont suivi, une suggestion est revenue : restreindre ou supprimer la métaprogrammation pour empêcher ce type d’attaque. Leo de Moura balaie l’idée sans détour.
L’élaborateur est, par conception, un composant non fiable. La sûreté du système ne peut pas reposer sur le refus, par un composant non fiable, de construire un terme malveillant. Un attaquant qui voudrait soumettre une preuve invalide peut aussi écrire directement des fichiers .olean ou modifier la mémoire, deux vecteurs qui contournent totalement l’élaborateur.
Le kernel doit rejeter les déclarations mal typées par lui-même, dans son propre processus. Cette séparation des responsabilités est l’un des grands avantages des termes de preuve. Vouloir colmater la brèche en réduisant la surface d’attaque de l’élaborateur reviendrait à déplacer le problème sans le résoudre.
Ce que le FRO a mis en place depuis
La Fondation Lean (FRO) n’a pas chômé. Des tests de régression pour l’exploit, ainsi que pour un cas connexe de paramètres non uniformes signalé par Arthur Adjedj, ont été intégrés à la Kernel Arena, la suite de tests du noyau.
Un correctif complémentaire (PR #14582) fait désormais en sorte que le kernel vérifie que les paramètres d’une occurrence imbriquée se comportent bien comme des paramètres, au lieu de simplement les re-vérifier.
Daniel Selsam, chez OpenAI, a assisté le FRO avec une IA spécialisée en cybersécurité. Résultat : d’autres erreurs de programmation ont été trouvées dans le kernel. Toutes ont été corrigées. Toutes étaient détectées par nanoda. Les PRs concernés sont #14607, #14608, #14609, #14613, #14615 et #14616. Les invariants du kernel ont également été renforcés (PRs #14621, #14631, #14632).
Côté infrastructure, comparator.live exécute désormais nanoda par défaut, et nanoda fait l’objet d’un suivi quotidien pour que lean-eval et comparator restent synchronisés avec les correctifs amont. Le FRO prend aussi contact avec des experts capables de trouver d’autres bugs, de développer de nouveaux kernels et de travailler sur la théorie ou sur des kernels formellement vérifiés.
Une confiance renforcée par la transparence
Le postmortem de Leo de Moura a été salué pour sa franchise. Là où un bug de cette nature aurait pu éroder durablement la crédibilité de Lean, la réaction rapide et documentée de l’équipe a produit l’effet inverse. La communauté, bien que secouée, semble sortir renforcée de l’épisode.
Le bug était cantonné à une fonctionnalité non couverte par la preuve de cohérence de Mario Carneiro dans lean4lean, une formalisation en Lean de la théorie des types de Lean. Cette preuve, encore en cours, ne couvre pas encore les types inductifs. Le bug aurait de toute façon été découvert lors de la finalisation de cette vérification.
L’incident illustre une réalité plus large : la sûreté des assistants de preuve est un enjeu critique, et la vérification formelle du kernel lui-même reste un objectif à atteindre. La transparence dont fait preuve l’équipe Lean est probablement le meilleur atout pour y parvenir.
Ce qu’il faut retenir
- Le bug #14576 permettait de faire accepter une preuve de
Falseau kernel de Lean via un défaut dans la gestion des types inductifs imbriqués à paramètres fantômes. - La faille n’était exploitable que par métaprogrammation, en contournant le frontend ; le bug est une erreur d’implémentation, pas un vice théorique.
- Deux bugs indépendants dans deux implémentations (kernel officiel et nanoda) étaient nécessaires pour laisser passer la preuve fautive de la conjecture de Collatz.
- L’équipe Lean a corrigé la faille en une heure, renforcé les invariants du kernel et fait appel à une IA de cybersécurité pour débusquer d’autres erreurs potentielles.
- La transparence du postmortem et la qualité de la réponse technique ont renforcé la confiance de la communauté plutôt que de l’affaiblir.
Vous utilisez Lean dans vos projets de formalisation ou vous vous intéressez à la sûreté des assistants de preuve ? N’hésitez pas à partager votre retour en commentaire ou à me contacter pour échanger sur ces sujets.
Sources
- Postmortem for Kernel Soundness Bug #14576, Billet officiel de Leonardo de Moura, créateur de Lean
- Are we stuck with Lean?, Discussion académique sur MathOverflow autour des implications du bug
- AI-Generated Lean Proof Exploits Collatz Kernel Bug, Article relayé par Digg illustrant l’exploitation concrète de la faille par une IA