The Collatz 'Disproof' That Beat Two Proof Checkers

On July 25, Ramana Kumar published a repository containing a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It compiled. #print axioms came back empty. And nanoda, an independent Lean proof checker written in Rust by Chris Bailey, accepted it too. Every signal the formal-methods community tells you to trust said the proof was real.

Three days later, Kiran Gopinathan boiled the trick down to a minimal proof of False and filed issue #14576 against the Lean 4 kernel. Leonardo de Moura pushed a fix one hour after the report; Joachim Breitner reviewed it and it merged the same day. De Moura's postmortem, published August 1, is unusually candid — and it reads less like a compiler bug report than like a security incident writeup. That's the real story here.

The bug itself

When Lean's kernel accepts a nested inductive declaration, it compiles the nesting away by generating auxiliary inductive types. The bug: if the nested type had phantom parameters — parameters declared in the type but never mentioned in any constructor field — those parameters vanished from the generated auxiliary type. Whatever arguments sat in those positions were never type-checked. An ill-typed argument there could walk the kernel into accepting a proof of False.

A phantom parameter is nothing exotic:

inductive Tag (α : Type) : Type
  | mk : Tag α   -- α never appears in a field

Nest something like that inside another inductive, hand the declaration straight to the kernel, and the α slot became a blind spot. De Moura is precise about the scope: this is an implementation bug, not a hole in Lean's type theory, and it's only reachable through metaprogramming that submits declarations directly to the kernel. The elaborator catches the ill-typed term in ordinary use, so nobody was going to trip over this writing normal tactic proofs.

Two bugs, one exploit

The formal-methods sales pitch has always leaned on defense in depth: keep the kernel small, and let independent checkers re-verify everything so a single implementation bug can't cost you soundness. Here's the uncomfortable part of this incident — the exploit beat the independent checker too.

nanoda accepted the fake disproof because of a second, unrelated bug: it skipped verifying type names in projection nodes. That bug had already been fixed a week earlier, but the exploit was deliberately crafted so that the expressions Lean's kernel never inspected were exactly the ones an outdated nanoda would wave through. De Moura's gloss is that independent checking still works, "since it required two distinct bugs in two implementations." True — and also a near miss that proves attackers will treat your checkers as attack surface, not as a formality.

The correlated-failure footnote is worse. lean4lean, the project to produce a formally verified Lean checker, ports the reference implementation — so its to-be-verified code contained the same bug, and its consistency proof doesn't cover inductive types yet. Implementation diversity only buys you safety when the implementations don't share lineage. Anyone who's watched a monoculture of forked TLS stacks ship the same parsing bug knows this lesson; theorem proving just learned it in public.

The response was security engineering

What happened next is the part worth copying. Regression tests for the exploit went into the Kernel Arena suite, including a related non-uniform-parameter case Arthur Adjedj raised during review. A follow-up PR (#14582) made the kernel verify that parameters of a nested occurrence actually behave as parameters. comparator.live now runs nanoda daily against current Lean, so the "independent checker is three versions stale" hole closes. And Daniel Selsam at OpenAI pointed a security-specialized AI at the kernel, which surfaced further programming mistakes — fixed across six PRs, with three more hardening kernel invariants.

Patch fast, add regressions, run continuous differential testing, invite a red team. That's CVE response, applied to a proof checker.

De Moura also shut down the predictable suggestion to restrict metaprogramming so the attack "isn't expressible." His reasoning is the correct security instinct: the elaborator is untrusted by design, and an attacker can write .olean files or patch memory and bypass it entirely. Soundness can't depend on an untrusted component politely declining to build a bad term. Validate at the trust boundary — the kernel — not upstream of it.

Paulson's rebuttal, and the honest trade-off

Two days after the fix, Lawrence Paulson published a pointed counterargument titled "Why is it all in the kernel?" His case: Lean's kernel is rich — nested inductives, primitive projections, bignum arithmetic — because richness buys speed, and every one of those features is trusted code that can harbor exactly this class of bug. Isabelle derives recursion and inductive definitions outside its kernel; HOL Light's tiny kernel has a decades-long soundness record, and Candle is a formally verified descendant of it. Rocq, which made the same rich-kernel trade as Lean, has its own history of soundness bugs in pattern matching and recursion to show for it.

Paulson's right about the trade-off, and it deserves saying plainly: Lean bought kernel-reduction performance — the thing that makes checking a four-million-line mathlib tractable — by enlarging its trusted base, and the interest on that loan is paid in incidents like this one. But the conclusion isn't that Lean chose wrong. It's that the choice converts soundness from a one-time argument into an ongoing operational discipline. The postmortem shows the Lean FRO accepting that bill, which is far better than pretending it doesn't exist.

What to actually do about it

If you write ordinary Lean, your accidental risk was near zero and remains so; the elaborator was never fooled. Upgrade past the July 28 toolchain and move on.

If you accept proofs from parties you don't trust — AI proof-generation pipelines, bounty submissions, external CI contributions — your threat model changed this week. Treat a proof artifact like hostile input to a parser. Re-check with an independent kernel, and check the checker's version too: this exploit specifically targeted a stale nanoda. Record the exact toolchain and checker versions alongside any "machine-checked" claim, because that claim is about a specific binary on a specific date, not a mathematical absolute.

The week's net result: one dented doctrine, one genuinely good precedent. Proof assistants now have adversaries with AI leverage and patience, and the community's first real incident response looked like mature security practice. Formal methods has joined the rest of software — it ships trusted code, and trusted code gets postmortems.