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 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. The bug: when the kernel eliminates a nested occurrence under an inductive type T with parameters Ds , and these parameters are phantom (not mentioned in constructor fields), they disappear from the generated auxiliary type and thus escape type checking.…