“This is an implementation bug, not a hole in Lean’s meta-theory.”
Nested inductive types with phantom parameters let ill-typed arguments slip past elimination, which was enough to prove False. It surfaced because someone published an AI-assisted disproof of the Collatz conjecture, which is the kind of result that only ever means the tool is broken. Kiran Gopinathan cut it down to a minimal proof of False and the patch merged within an hour. The bug needed metaprogramming to reach, so ordinary proofs were never affected, and the postmortem states the limits without spin.