On 25 July, Ramana Kumar published a machine-assisted disproof of the Collatz conjecture. It type-checked in Lean. Since Collatz has resisted every serious attack for eighty-odd years, and since a counterexample would have been extraordinary news on its own, the interesting question was not whether the proof was right. It was which part of the stack had lied.

The answer, three days later, was the kernel. Leo de Moura published the postmortem on 1 August, and it is worth reading in full for the parts that are less flattering than the fix.

RelatedGitHub Ships Native Stacked Pull Requests in Preview

What breaks when a proof assistant is unsound?

Lean's whole value proposition rests on a small trusted core. You can write arbitrarily clever tactics, elaborate arbitrarily hairy syntax, and generate proof terms by any means you like, including a language model. None of that has to be trusted, because at the end a compact kernel checks the resulting term against the type theory. If the kernel says yes, the theorem holds.

So a kernel soundness bug is the one failure mode the design has no answer for. It means the kernel said yes to something false. And "something false" is not a figure of speech here: Kiran Gopinathan reduced Kumar's Collatz artefact to a minimal derivation of False, which in a system with the principle of explosion means every statement is provable. Gopinathan filed it as issue #14576 on 28 July.

The actual defect

The bug lived in the kernel's handling of nested inductive types that carry phantom parameters, meaning parameters that never appear in any constructor's field types. Because nothing in the constructors mentions them, these parameters were being dropped during elimination. Once a parameter disappears from the eliminator's expectations, arguments that should have been rejected as ill-typed sail through, and from there you can construct a term that inhabits the empty type.

How a phantom parameter escaped Lean's kernel type check A three-stage diagram. Stage one: a nested inductive type is declared with a phantom parameter, a parameter mentioned in the type signature but in none of the constructor field types. Stage two: during elimination the kernel drops the phantom parameter, because nothing in the constructors depends on it. Stage three: with the parameter gone, ill-typed arguments pass the check, and a term inhabiting the empty type can be constructed, yielding a proof of False. A side panel records that the path was reachable only by sending inductive declarations directly to the kernel through metaprogramming, since the frontend's own argument checking blocked it. LEAN ISSUE #14576 · KERNEL SOUNDNESS 1 · DECLARE Nested inductive with a phantom parameter, unused by any constructor 2 · ELIMINATE Parameter vanishes the eliminator stops expecting it at all 3 · EXPLODE Ill-typed args pass ⊢ False every theorem follows Reachable only through metaprogramming Declarations had to be sent straight to the kernel. The frontend's argument checking blocked the ordinary path. An implementation bug, not a hole in Lean's meta-theory. The type theory was never in question. The code implementing it was. genztech.blog
Fig 1 Phantom parameters are dropped during elimination, and everything downstream stops checking for them.

How exploitable was it, really?

Less than the headline suggests, and the distinction matters. The bug was reachable only by sending inductive declarations directly to the kernel through metaprogramming. Lean's frontend performs its own argument checking, and that checking blocked the ordinary path. You could not stumble into this by writing normal Lean, and no result in mathlib was ever at risk from an accidental trigger.

De Moura's framing is that this was an implementation bug, not a hole in Lean's meta-theory. That is the correct and important distinction. The type theory Lean implements was not shown to be inconsistent. A particular piece of code implementing it got a case wrong. Those are different categories of problem, and only the second one is fixable with a patch.

What it does undermine is a weaker but widely-held assumption: that a proof artefact which type-checks in Lean can be trusted without knowing how it was produced. If the producer had metaprogramming access, "it checks" was not, for these five days, a complete argument.

  1. Jul 25The Collatz artefact appears Ramana Kumar publishes an AI-assisted disproof that type-checks
  2. Jul 28Reduced to a minimal case Kiran Gopinathan derives False and files issue #14576
  3. Jul 28Fix pushed within the hour PR #14577, reviewed and merged by Joachim Breitner
  4. Jul 28+Patch releases ship plus regression tests and hardened kernel invariants
  5. Aug 1Postmortem published de Moura details the defect and the process changes

The uncomfortable part

Lean has an independent checker, nanoda, precisely so that a kernel bug is not a single point of failure. Two implementations disagreeing is the whole mechanism. In this case nanoda did not catch the exploit, because nanoda had its own separate and unrelated bug.

That is a nastier finding than the original defect. Independent verification protects you exactly to the degree that the implementations fail independently, and two checkers written against the same specification, by people reading the same documents, are correlated in ways that are hard to see until something like this happens. The Lean FRO's response has been to run nanoda on comparator.live by default rather than on request, harden kernel invariants across several PRs, add regression tests, and bring in security researchers to look for more. Making the second checker run automatically is the right first move. Whether two checkers is enough diversity is now an open question rather than an assumed answer.

RelatedDebian Votes on Four Rival Rules for AI Contributions

What this means for AI-assisted mathematics

The obvious reading is that AI proof search broke the trusted core, and it deserves some care. Nothing here required a language model. A sufficiently determined human with metaprogramming access could have found the same path, and people have found comparable bugs in Coq and Isabelle over the years without any machine help.

What the AI angle genuinely changes is throughput. Machine-generated proof search explores strange, adversarial corners of a system's behaviour at a volume no human team matches, and it does so without the tacit sense of "that's not how you're supposed to write it" that keeps human mathematicians on well-trodden paths. That is precisely the property you want in a fuzzer. Lean's kernel has now been fuzzed by a process that does not know what idiomatic means, and it found something in five years of accumulated code.

Expect more of these. Expect most of them to be implementation bugs rather than meta-theory holes, and expect the ones that matter to be found the way this one was: by someone taking an implausible result seriously enough to minimise it, rather than dismissing it.

Our take

The handling here was close to exemplary and the timeline proves it. Issue filed and fix pushed inside an hour, reviewed by a second person, patch releases out the same day, a public postmortem within four days that volunteers the embarrassing detail about nanoda rather than burying it. Compare that against how most software vendors handle a soundness-class defect and the gap is enormous.

The lesson is not that formal verification failed. It is that "verified" was always a claim about a specific implementation, and the trusted computing base of a proof assistant includes the kernel's C++ and its build, not just the type theory on paper. Everyone working in the field knew that in the abstract. This is what it looks like concretely, and the useful outcome is that the second checker now runs by default.

What to watch · next 12 months
  • What the security review turns up. The FRO has engaged external researchers. A kernel that has never been adversarially audited rarely yields exactly one finding.
  • Whether nanoda gets company. Two correlated checkers is thinner assurance than it looked last week. A third implementation from a different lineage would say more.
  • Mathlib's posture on provenance. Whether the community starts asking how a contributed proof was produced, not just whether it checks.
  • Coq and Isabelle. Phantom parameters in nested inductives are not a Lean-specific concept. Somebody is going to go looking.
Primary sources

Original analysis by GenZTech. Technical details drawn from the published postmortem and the linked issue and pull request.