Lean's Proof Kernel Fell to an AI-Assisted 'Disproof' of Collatz

A soundness bug in the Lean theorem prover’s kernel let a proof of False slip past type checking, and it surfaced in dramatic fashion: on July 25 Ramana Kumar published an AI-assisted, sorry-free repository claiming to disprove the Collatz conjecture. The ‘proof’ was bogus, but it worked because the kernel mishandled nested inductive types whose parameters are phantom — never mentioned in constructor fields. Those parameters dropped out of the generated auxiliary type and escaped checking, so an ill-typed term in that slot could be accepted. Kiran Gopinathan boiled the exploit down to a minimal proof of False and filed issue #14576 on July 28; the Lean FRO shipped a fix one hour later. Crucially, the flaw is an implementation bug reachable only by feeding declarations to the kernel directly through metaprogramming — the elaborator frontend catches it, and Lean’s underlying meta-theory is not in question.

The more unsettling detail is that nanoda, the independent Rust re-implementation of the kernel that many rely on as a second opinion, also waved the malformed proof through. That took two entirely separate bugs: the official kernel skipped a check on nested inductives, while nanoda failed to verify the type name in a projection node. The exploit was constructed so the one expression the kernel never inspects was exactly the one an older nanoda would accept. nanoda’s bug had been reported and patched a week earlier, and while the timing looks coincidental, no one can fully rule out that the model had seen that report — raising the prospect that capable models are now good enough to find these defects on their own.

The practical takeaway is that cross-checking with an independent kernel still holds up, since defeating it required distinct flaws in two implementations, but only if users run current versions of both; Mario Carneiro’s lean4lean formalization inherited the same kernel bug and would have caught it once its verification of inductive types was complete. The team pushed back on calls to strip out metaprogramming, arguing that the elaborator is untrusted by design and that an attacker could bypass it anyway by writing .olean files or editing memory — soundness has to live in the kernel itself. In response the FRO added regression tests, tightened parameter checks, and hardened kernel invariants; notably, an OpenAI security-specialized AI run by Daniel Selsam turned up several more kernel bugs, all metaprogramming-only, all now fixed, and all of which nanoda would have flagged.