Lean postmortem: an AI Collatz 'disproof' proved False in the kernel
A phantom-parameter hole let ill-typed terms prove False; a follow-up AI sweep found 5 more kernel bugs. Patches shipped, meta-theory intact.
Copy markdown
How it broke: phantom parameters slipped past the checker
The hole sat in Lean's kernel handling of nested inductive types with phantom parameters — ones a type declares but never uses in its constructors. During elimination they dropped out of auxiliary types, so an ill-typed argument could make the kernel accept a proof of False. It only fires through direct metaprogramming; the normal frontend catches it, which is why de Moura calls it “an implementation bug, not a hole in Lean's meta-theory.”
An AI Collatz 'disproof' was the smoke
The trail started July 25, when Ramana Kumar posted an AI-assisted “disproof” of the Collatz conjecture; on July 28 Kiran Gopinathan boiled it down to a bare proof of False and filed #14576, fixed within the hour by PR #14577. The lesson for anyone leaning on AI for math or formal specs: the failure mode isn't a wrong answer, it's a proof that sails through a buggy verifier.
Then a security-focused AI sweep found 5 more
After the fix, the Lean FRO pointed AI at its own kernel and surfaced five additional soundness bugs — every one exploitable only via metaprogramming, and every one already caught by an independent checker. They shipped regression tests and hardened parameter verification (PR #14582). Expect more of these to surface now that people are aiming AI at verifiers.
Two kernels beat one: nanoda caught what Lean missed
Chris Bailey's independent Rust kernel, nanoda, flagged the bug — and turned out to carry its own unrelated hole (it wasn't checking the type name in a projection node), patched a week earlier. If you're trusting a high-stakes or AI-generated proof, run it through a second, independent kernel rather than the official one alone.
What to do: update, and trust the green check a little less
Fresh patch releases of both the official kernel and nanoda are out — update before you rely on any newly minted proof. The kernel code has been near-unchanged for 5+ years and the meta-theory holds, so this isn't a reason to abandon formal verification, just a reminder that a passing verifier is only as sound as its implementation.