A machine-assisted disproof of the Collatz conjecture appeared on 25 July and type-checked in Lean. It was wrong, and it was wrong in the most interesting way possible: it had found a genuine soundness bug in the proof assistant's kernel, letting False be derived through metaprogramming.
Read the full story: An AI Collatz ‘disproof’ exposed a hole in Lean's kernel →
Transcript
On the twenty fifth of July, Ramana Kumar published a machine assisted disproof of the Collatz conjecture. It type checked in Lean. Now, Collatz has resisted every serious attack for eighty odd years, so the interesting question was never whether the proof was right. It was which part of the stack had lied. The answer was the kernel. Lean's whole value proposition is that you can generate proofs by any means you like, including a language model, because a small trusted core checks the result at the end. If the kernel says yes, the theorem holds. So a kernel bug is the one failure mode the design has no answer for. Kiran Gopinathan reduced the artefact to a minimal proof of False, which means every statement becomes provable. The cause was nested types carrying parameters that no constructor mentions. Those were silently dropped, and ill typed arguments sailed through. The fix was merged within the hour. But here is the uncomfortable part. Lean has a second independent checker precisely so this cannot happen, and it missed the exploit, because it had its own separate bug.