A critical soundness bug in the Lean theorem prover kernel was discovered and patched within one hour after researchers demonstrated an AI-generated "disproof" of the Collatz conjecture.

On July 25, Ramana Kumar published a repository containing what appeared to be a valid proof disproving the famous mathematical conjecture. The proof exploited a bug in Lean's kernel handling of nested inductive types with phantom parameters.

Kiran Gopinathan reduced the exploit to a minimal proof of False and opened issue #14576 on July 28. Leonardo de Moura, Lean's creator, pushed a fix within an hour.

The vulnerability

The bug occurred when the kernel eliminated nested occurrences under inductive types with phantom parameters — parameters not mentioned in constructor fields. These parameters would disappear from generated auxiliary types, allowing ill-typed arguments to bypass type checking.

The vulnerability was only reachable through metaprogramming by sending inductive declarations directly to the kernel. Lean's frontend normally catches such ill-typed terms.

Surprisingly, the exploit also passed nanoda, an independent Rust-based Lean checker by Chris Bailey. This required exploiting two separate, unrelated bugs in both implementations.

The nanoda bug had been fixed a week before the Lean bug was reported. Joachim Breitner suggested the timing coincidence reflects the availability of AI models capable of finding such vulnerabilities.

Response and hardening

Daniel Selsam at OpenAI assisted the Lean Foundation with a cybersecurity-specialized AI that identified additional programming mistakes in the kernel. All discovered bugs were caught by nanoda and have been patched.

The foundation added regression tests to the Kernel Arena and implemented stricter parameter validation. The comparator.live service now runs nanoda by default with daily tracking.

Mario Carneiro's lean4lean project — a Lean formalization of Lean's type theory — was also affected, as it ports the reference implementation's inductive handling.

De Moura emphasized that removing metaprogramming would be misguided, as soundness must not depend on untrusted elaborator components. The kernel must reject ill-typed declarations independently.