Postmortem for Kernel Soundness Bug #14576
Developers have patched a soundness bug in the Lean kernel that allowed for the acceptance of invalid proofs, including a flawed AI-assisted attempt at the Collatz conjecture. The issue was identified as an implementation error in how the kernel handles nested inductive types.
Why it matters
The incident highlights the risks of using AI in formal verification and the importance of rigorous kernel-level type checking in mathematical software.
A soundness bug in the Lean kernel ( #14576 ) was reported and fixed during the week of July 27. It has had visibility on Zulip and social media (e.g., X, LinkedIn, and Mastodon).
On July 25, Ramana Kumar published a repository containing a sorry -free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576 . We pushed a fix one hour after the report ( #14577 ). Joachim Breitner reviewed it and suggested improvements, and it was merged. New patch releases are out.
Get smarter about the news
Sign up free for a feed built around what you actually care about, Dive Deeper research on any story, and the full text of every article.
Create free accountAlready have an account? Sign in