The Collatz 'Disproof' That Beat Two Proof Checkers

On July 25, Ramana Kumar published a repository containing a sorry-free Lean "disproof" of the Collatz conjecture, produced with AI assistance. It type-checked. It also passed nanoda, an independent reimplementation of Lean's kernel in Rust. Three days later Kiran Gopinathan boiled the repo down to a clean, axiom-free proof of False and filed issue #14576 against Lean 4. Leonardo de Moura pushed a fix within an hour, and this week published a postmortem that reads like a security incident report — because that's what it is.

The interesting part isn't that the kernel had a bug. Every proof assistant's kernel has had bugs; Coq, Isabelle, and Agda all carry lists of historical soundness holes. The interesting part is that this exploit required two unrelated bugs in two independently written checkers, and it found both.

Two blind spots, one expression

The kernel-side bug lived in Lean's support for nested inductive types. When the kernel compiles away a nested occurrence under an inductive type whose parameters are phantom — declared, but never mentioned in any constructor field — those parameters get dropped from the generated auxiliary types. Dropped, and therefore never type-checked. An ill-typed argument in that position sails straight through. The minimized exploit leans on this to forge a projection whose structure name doesn't match the value being projected, and from that mismatch a proof of False falls out.

nanoda, written by Chris Bailey precisely to catch official-kernel bugs like this one, did check the spot Lean missed. But it had its own hole: it didn't verify the type name in projection nodes. The exploit threaded both needles at once — the expression Lean's kernel never inspects is exactly one the old nanoda accepted. In a small twist, Jeremy Chen had fixed nanoda's bug a week before the report landed, independently of the Collatz repo.

Two things keep this out of crisis territory. First, it's an implementation bug, not a hole in Lean's type theory — the fix (PR #14577, hardened further in #14582) makes the kernel actually check that nested-occurrence parameters behave as parameters. Second, the bug was only reachable through metaprogramming, by handing an inductive declaration directly to the kernel. You couldn't trip it from ordinary surface Lean, which is why years of mathlib development never hit it.

Redundancy is not independence

Lawrence Paulson, of Isabelle fame, used the incident to press a long-standing critique: Lean's kernel does too much (nested inductives included), and he is "not aware of a single instance where an independent proof checker detected a soundness error that had passed through the kernel of a proof assistant." If soundness is your top concern, he says, use HOL Light or HOL4, whose kernels define everything from primitive axioms.

He's half right, and the half he's wrong about is the more instructive one. In the aftermath, Daniel Selsam at OpenAI ran an AI-assisted security review over the Lean kernel and turned up more programming mistakes — six additional fix PRs, all in metaprogramming-only territory. Every one of those was caught by nanoda. The independent checker isn't useless; it demonstrably catches real kernel bugs. What it can't do is stand up to an adversary who gets to query both checkers and search for the intersection of their blind spots. Random bugs land in one implementation or the other. A search process that iterates until everything says "accepted" lands, with uncanny reliability, in the overlap.

That's the real lesson, and it's a familiar one from security engineering: an ensemble of verifiers is only as strong as the intersection of their weaknesses once the attacker can use them as an oracle. We don't know whether Kumar's AI pipeline was deliberately hunting soundness bugs or simply reward-hacked its way into one while chasing a headline theorem. It doesn't matter. Joachim Breitner suggested in the postmortem discussion that the timing is no coincidence — models strong enough to find bugs like this have only just arrived. De Moura was blunter in an interview with Machine Learning Street Talk: "This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels."

The response is the actual endorsement

Judged as an incident response, the Lean FRO's week was close to exemplary: minimized repro to merged fix in one hour, a stronger invariant check behind it, regression tests, several follow-up hardening PRs, an adversarial AI review, and comparator.live now running nanoda by default with daily tracking. De Moura is also explicit about the endgame: Mario Carneiro's lean4lean — a formalization of Lean's type theory plus a proof that the kernel implements it — doesn't yet cover inductive types, and finishing that part would have surfaced this exact bug. Notably, the unverified prototype kernel in lean4lean shared the same flaw, which is about as clean an argument for machine-checked kernel verification as you'll ever get.

If you ship on Lean

For most users this changes nothing operationally: upgrade to a current toolchain and move on. The people who need to sit up are the ones building pipelines where Lean proofs are a trust boundary — AlphaProof-style AI provers, proof marketplaces and bounties, and systems like AWS's Cedar authorization language, whose semantics are modeled in Lean. Three concrete takeaways for them:

• Treat third-party proof artifacts as untrusted code, full stop. Elaborating a .lean file executes arbitrary metaprograms. Even post-fix, that's a far larger attack surface than any kernel bug — sandbox elaboration before you worry about soundness.
• Re-check final environments with external tools (lean4checker, nanoda) on patched versions, and assume checker diversity buys you protection against accidents, not against adversarial search. #print axioms would not have flagged this proof; it was axiom-free by construction.
• If a machine-generated result is extraordinary, the checker's verdict is the beginning of scrutiny, not the end. Everyone doubted the Collatz repo on sight — that instinct is now a required part of the workflow.

The deeper shift is cultural. For forty years, "the kernel accepted it" was the strongest correctness claim computing could offer, and it earned that status against human proof authors who weren't trying to cheat. AI provers change the threat model from correctness to security: kernels are now attack surfaces with motivated, tireless adversaries, and they need security-grade engineering — fuzzing, adversarial review, and ultimately verified implementations. Lean's bet on lean4lean looks less like an academic flourish now and more like the only durable answer. This incident didn't weaken the case for formal verification. It ended the era of running proof checkers on the honor system.