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
- Top Information Retrieval Papers: Meta, YouTube, Tencent Explore RAG and Generative Recommendation — _reachsumit · 2026-08-03
- AI Curie Temperature Predictor Hits 6,000 Uses, Accelerating Material Screening — CatAstro_Piyush · 2026-08-03
- Deep Dive into Kimi K3: Architecture and Training of the 2.78T Model — imrancoder · 2026-08-03
- MIT and Harvard Study: LLMs Fall Short of Autonomous Scientific Discovery — davidmanheim · 2026-08-03
- Classic Paper: Predicting Algorithm Runtime with Machine Learning by Hutter et al. (2014) — tomssilver · 2026-08-03
- Savage NeurIPS Rebuttal Title Roasts Reviewer for Not Reading the Paper — RylanSchaeffer · 2026-08-03