Postmortem for Lean Kernel Soundness Bug #14576

On July 25, Ramana Kumar published a repository containing a supposedly valid disproof of the Collatz conjecture, created with AI assistance. However, it was discovered that the proof relied on a bug in Lean's kernel handling of nested inductive types. Kiran Gopinathan fixed the issue and opened issue #14576, which was promptly addressed and fixed one hour later with patch #14577. Joachim Breitner reviewed the fix and proposed improvements, leading to the patch's eventual merge.

The bug allowed ill-typed arguments to bypass type checking, potentially enabling the kernel to accept a proof of False through metaprogramming. This vulnerability is only reachable by directly sending the inductive declaration to the kernel, which the frontend usually catches. The bug existed due to a missing check in the kernel's nested inductive type support, while an independent kernel named nanoda, implemented in Rust by Chris Bailey, correctly caught the issue but failed to verify the type name in a projection node.

The kernel bug was subsequently fixed in patch #14582, which checks that the parameters of a nested occurrence behave as expected. Additionally, other programming mistakes in the Lean kernel were identified and corrected by Daniel Selsam, with the assistance of an AI specialized in cybersecurity from OpenAI. All of these bugs were only exploitable through metaprogramming and required two distinct vulnerabilities in separate implementations.

Users relying on kernel-based checking still need to ensure they have the latest versions of both Lean and nanoda. While the practical consequences are mitigated, further improvements are being made, including hardening kernel invariants and supporting experts who can find additional bugs, develop new kernels, and work on verified implementations.