Summary
Lean fixed a soundness bug in its kernel after an invalid, AI-assisted Collatz disproof exposed a path to making it accept a proof of False. The postmortem describes a separate flaw in an older independent checker and the fixes and safeguards that followed.
Lean fixed a soundness bug in its kernel after an invalid, AI-assisted attempt to disprove the Collatz conjecture exposed a way to make the proof checker accept a proof of False. In a postmortem, Lean FRO’s Leonardo de Moura says the issue was reported and fixed during the week of July 27, with new patch releases issued.
A proof assistant such as Lean checks formal proof terms with a kernel: a small, critical part of the system that verifies whether a proof follows from the stated rules. The reported flaw was in how that kernel handled certain nested inductive types, not in Lean’s underlying meta-theory.
How the kernel bug worked
On July 25, Ramana Kumar published a repository containing a sorry-free purported disproof of the Collatz conjecture, produced with AI assistance. It was not a valid proof: it exploited the kernel bug. On July 28, Kiran Gopinathan reduced the exploit to a small proof of False and reported it as issue #14576. Lean pushed a fix about an hour after the report; Joachim Breitner reviewed it, and the change was merged.
The flaw involved nested occurrences of inductive types. In a particular case, an inductive type’s parameters could be phantom—that is, not mentioned in its constructor fields. When the kernel generated an auxiliary type while handling a nested occurrence, those parameters could disappear from that type and escape checking. An ill-typed argument in that position could then be used to make the kernel accept a proof of False.
The exploit required metaprogramming to send an inductive declaration directly to the kernel. Lean’s frontend checks the arguments and catches the ill-typed term in the ordinary path. But the frontend, or elaborator, is not meant to be a security boundary: the kernel must reject ill-typed declarations itself, even if they arrive through a different route. De Moura characterises this as an implementation bug rather than a gap in Lean’s meta-theory.
Why an independent checker also accepted it
The original repository also passed a week-old version of nanoda, an independent Lean kernel written in Rust by Chris Bailey. The postmortem identifies a separate bug in that version: nanoda checked the relevant nested-inductive case, but failed to verify the type name in a projection node. The exploit used an expression that the official kernel did not inspect and that the older nanoda accepted. That nanoda bug had been reported and fixed a week before the Lean kernel issue.
The episode therefore involved two distinct bugs in two implementations. De Moura says independent-kernel checking remains useful, but users relying on it need current versions of both Lean and nanoda. The fix for Lean includes regression tests for the exploit and for a related non-uniform-parameter case. A follow-up change, #14582, makes the kernel check that parameters of a nested occurrence actually behave as parameters.
The postmortem also describes further kernel work. Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialised in cybersecurity, which found other programming mistakes; the project says those were fixed and caught by nanoda. Lean also hardened kernel invariants and began running and tracking nanoda regularly in comparator.live.
A related formalisation project, lean4lean, was affected because its inductive-type handling is ported from the reference implementation. Its ongoing consistency proof does not yet cover inductive types; de Moura says the bug would have been found while completing verification of that part.
The postmortem does not determine whether the model that assisted with the Collatz repository had seen the earlier nanoda report. Kumar considered the timing coincidental but could not rule out prior exposure; de Moura also records the possibility that stronger models are now capable of finding this class of bug.