AI-Assisted Pseudo-Proof Exploits Soundness Bug in Lean Kernel
AlexKontorovich · x · 2026-08-03
Leonardo de Moura, a core developer of the Lean theorem prover, published a detailed postmortem on kernel soundness bug #14576.
The Incident
On July 25, Ramana Kumar published an AI-assisted, sorry-free repository claiming to "disprove" the Collatz conjecture. It actually exploited a flaw in how the Lean kernel handles nested inductive types. Kiran Gopinathan later reduced it to a minimal proof of False and opened issue #14576. The team pushed a fix within an hour.
The Bug
When the kernel eliminates a nested occurrence under an inductive type with phantom parameters, those parameters disappear from the generated auxiliary type, escaping type checking. An ill-typed argument in that position could trick the kernel into accepting a proof of False. This bug is only reachable via metaprogramming by sending declarations directly to the kernel, and is an implementation bug, not a hole in Lean's meta-theory.
Why External Checkers Missed It
The proof initially passed nanoda, an independent Rust-based external checker. This was due to two unrelated bugs: the official kernel missed a check for nested inductives, while nanoda checked that spot but failed to verify the type name in a projection node.
More from Research
- Simplex Diffusion Models paper talk by EPFL/DeepMind's Justin Deschenaux on Oct 19 — ArnaudDoucet1 · 2026-10-16
- Meituan LongCat team's Data World synthesizes data environments to train data agents — meituan-longcat · 2026-10-16
- FDE-Gym benchmark shows huge gap on real AI delivery tasks: top model scores 0.563 — DeepLethe · 2026-10-16
- ForcingBooster halves computation of autoregressive video diffusion with patch-wise denoising — VAST-AI · 2026-10-16
- Baidu open-sources FlashMask: up to 1.55x faster than FlashAttention-4 for long-context training — BaiduResearch · 2026-10-16
- SemEval-2027 Task 9 opens: multimodal news framing analysis across 4 languages — preslav_nakov · 2026-10-16