Lean kernel soundness bug #14576

On 25 July 2026 Ramana Kumar published a Lean project that appeared to disprove the Collatz conjecture without any sorry or extra axioms, and that passed both Lean’s reference kernel and nanoda, an independent checker written in Rust. It had been produced with AI assistance; the README does not name a model. Three days later Kiran Gopinathan reduced the trick to a short, axiom-free proof of False and filed lean4 issue #14576. Leonardo de Moura opened a fix within two hours, and it was merged and released as Lean 4.32.2 that day.

De Moura’s postmortem explains that the exploit needed two unrelated bugs. The official kernel lost phantom parameters of nested inductive types, so they escaped type checking. Nanoda did check that, but did not verify the type name in a projection node. Lean4lean, a third checker, had copied the reference logic. Daniel Selsam of OpenAI then pointed a security-focused AI at the kernel and found six more implementation bugs, fixed on 30–31 July. Nanoda already rejected all six.

De Moura told Machine Learning Street Talk: “This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels.” In September Milo Moses warned on LessWrong that a Lean check alone should not establish confidence in AI results such as OpenAI’s Navier–Stokes proof.

On 9 Oct 2026, three days after OpenAI’s 722-manuscript release, Thomas Hales (who led the Flyspeck formal proof of the Kepler conjecture) published a guest post on Terence Tao’s blog. He named the period the “Summer of Soundness Bugs” and said another bug produced “a short illicit proof of the Kepler conjecture in Lean”. He listed three defences: cross-checking with many independent kernels (about 25 exist), formally verified kernels such as Candle and Joachim Breitner’s Con-Leche (whose code and consistency proof were generated by Claude), and better metatheory for Lean’s type theory.

“Verified in Lean” has become the main evidence behind AI labs’ math claims: OpenAI’s Navier–Stokes blow-up, 300 of 719 results in its October release, and Anthropic’s formal-math repository. This episode shows that the checker itself is an attack surface. AI systems that search hard for a proof may find a kernel bug more easily than a real proof. The mitigations are multiple independent kernels, verified kernels, and human audit that the formal statement matches the problem.