Aug 1, 2026
The Collatz kernel-soundness episode
Model / AI: Not specified
debunked
an AI-assisted sorry-free Lean "disproof" of Collatz stood for about three days, 25 to 28 July, by exploiting a phantom-parameter bug in the kernel's nested inductive types, and cleared the independent Nanoda checker by hitting a second, separate bug; Kiran Gopinathan reduced it to a proof of False and the Lean team patched it within an hour.
Source read 2026-09-08. Read the Lean maintainer’s postmortem describing the kernel bug and the separate outdated-nanoda bug. No checker was rerun.