Lean kernelの健全性バグ #14576 事後分析
Original : Postmortem for Kernel Soundness Bug #14576
Pourquoi c'est important
Ce cas illustre l'importance de l'indépendance des vérificateurs formels et de leur mise à jour régulière.
Le 28 juillet 2026, un bug de soundness dans le noyau de Lean a été signalé et corrigé en une heure. Ramana Kumar avait publié le 25 juillet une "réfutation" de la conjecture de Collatz sans sorry, exploitant ce bug via du métaprogramming.
Le 25 juillet 2026, Ramana Kumar a publié un dépôt contenant une prétendue réfutation de la conjecture de Collatz générée avec l'aide de l'IA, sans utiliser sorry. Il ne s'agit pas d'une preuve valide : elle exploite un bug dans la gestion des types inductifs imbriqués du noyau Lean. Le 28 juillet, Kiran Gopinathan a réduit l'exploit à une petite preuve de False et ouvert l'issue #14576. Un correctif (#14577) a été publié une heure après le signalement, puis revu par Joachim Breitner et mergé.
Le bug : lors de l'élimination d'une occurrence imbriquée sous un type inductif T avec des paramètres fantômes (non mentionnés dans les champs des constructeurs), ces paramètres disparaissent du type auxiliaire généré, échappant ainsi à la vérification de type. Ce chemin n'est accessible que via le métaprogramming, le frontend bloquant les termes mal typés normalement.
L'outil de vérification externe nanoda présentait lui aussi un bug distinct et indépendant, signalé par Jeremy Chen et corrigé une semaine avant la découverte du bug Lean. La preuve exploitait les deux failles simultanément. lean4lean de Mario Carneiro, en cours de formalisation, était également affecté car il porte l'implémentation de référence. Des tests de régression ont été ajoutés au Kernel Arena, et un PR de suivi (#14582) renforce les vérifications.