The Collatz 'Disproof' That Beat Two Proof Checkers
Inside Lean soundness bug #14576, the one-hour fix, and why machine-checked now comes with a patch cadence.
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.
Sources & further reading
- Postmortem for Kernel Soundness Bug #14576 — leodemoura.github.io
- Kernel accepts wrong-structure projections, allowing an axiom-free proof of False — github.com
- fix: missing check at kernel inductive declaration — github.com
- Why is it all in the kernel? — lawrencecpaulson.github.io
Ji-ho covers the increasingly tangled overlap between cloud architecture and security, drawing on a background as a penetration tester to keep his reporting grounded in real-world attack paths. He never lets a vendor claim go unquestioned and insists that every buzzword come with a proof of concept.
Discussion 4
this hits close to home. we had a similar moment in one of our cryptographic libraries where an unsound tactic quietly slipped through—our CI passed, the tests passed, and it took a community audit to catch it. the terrifying part wasn't the bug itself, it was that we'd built trust around tooling that was quietly broken. lean's moving fast to patch, which is good, but it surfaces something we don't talk about enough: formal verification tools need the same release discipline and transparency as cryptographic libraries, maybe more so.
okay so the proof checker itself had the bug, not the proof. that's simultaneously worse and way more interesting than i thought
I'm skeptical that this was really AI-assisted in any meaningful way — the exploit looks like standard dependent-type shenanigans that would trip up any system, not something a language model would stumble into. What matters more is that Lean 4 had a soundness bug that sat unfound until someone manually constructed a minimal example. That's the real gap: we're treating formal verification as solved once the checker accepts something, but the checkers themselves need continuous hardening.
you're right that the ai angle is kind of a red herring, but i'd flip the causality: the bug wasn't found earlier because nobody was *generating* 500-line proof attempts at scale. we had the same soundness holes in our z3 integration for years until a fuzzer finally produced the right sequence of tactics. it's not that language models are magically finding gaps—it's that they're providing free infinite monkeys at the keyboard. the real win here is that the feedback loop was three days, not three years.
