Lean Kernel Soundness Bug #14576 Postmortem
Original: Postmortem for Kernel Soundness Bug #14576
Why This Matters
A dual-bug exploit bypassing both official and independent Lean proof checkers highlights critical gaps in formal verification tooling.
On July 25, 2026, Ramana Kumar published a sorry-free Collatz conjecture disproof exploiting a Lean kernel bug. Kiran Gopinathan reduced it to a proof of False on July 28; a fix was pushed within one hour. New patch releases are now available.
A soundness bug (issue #14576) in the Lean proof assistant's kernel was reported and fixed during the week of July 27, 2026. On July 25, Ramana Kumar published a repository containing a sorry-free 'disproof' of the Collatz conjecture, produced with AI assistance. The proof exploits a bug in the kernel's handling of nested inductive types: when the kernel eliminates a nested occurrence under an inductive type T with phantom parameters (not mentioned in constructor fields), those parameters disappear from the generated auxiliary type, allowing an ill-typed argument to make the kernel accept a proof of False. The bug is reachable only through metaprogramming by sending an inductive declaration directly to the kernel; the frontend catches the ill-typed term. The fix (#14577) was pushed one hour after the report, reviewed by Joachim Breitner, and merged. The external checker nanoda also contained a separate, unrelated bug—reported by Jeremy Chen and fixed one week earlier—allowing the malicious proof to pass both checkers simultaneously. lean4lean, Mario Carneiro's Lean formalization of Lean's type theory, was also affected since its inductive handling is ported from the reference implementation. The Lean FRO has added regression tests to the Kernel Arena and opened follow-up PR #14582 to strengthen parameter checks.