Lean theorem prover kernel soundness bug exploited by AI-generated fake Collatz proof, discovered July 25-28, fixed within one hour; nested inductive type checking flaw bypassed both main kernel and external checker nanoda due to separate coinciding bugs.

Postmortem for Kernel Soundness Bug #14576 — Leonardo de Moura

2026-08-01 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). What happened 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...