AI-Assisted Collatz Disproof Invalidated by Lean Kernel Bug
The incident shows that even a trusted proof assistant like Lean can be fooled by crafted declarations that exploit kernel bugs, undermining the reliability of AI-assisted formal proofs.
Reporting from 1 source: GIGAZINE.
A project claiming to disprove the Collatz conjecture with AI assistance was accepted by the theorem prover Lean, but the proof exploited a bug in Lean's kernel. Lean developer Leonardo de Moura published a postmortem explaining the proof is invalid. The bug allowed the kernel to accept the proposition False, meaning any conclusion could be derived. The issue was reported on July 28 and involved nested inductive types and phantom type parameters.
Raman Kumar, a formal verification specialist, published a GitHub project on July 25 claiming to have disproved the Collatz conjecture with AI assistance. The project did not present a specific counterexample but asserted in Lean that a number exists which never reaches 1.
Lean's design routes user code through an elaborator and then a kernel that checks type consistency. The project avoided the 'sorry' placeholder and extra axioms, appearing to be a valid formal proof. However, Kumar found that Lean could be made to accept the proposition False, which is unrelated to the Collatz conjecture.
Researcher Kiran Gopinathan condensed the issue into a small reproduction and reported it to the Lean team on July 28. The bug lay in the kernel's handling of nested inductive types, where phantom type parameters were omitted from auxiliary types, allowing mismatched arguments to evade checks. Exploiting it required metaprogramming to send crafted declarations directly to the kernel.
Synthesized by Yomimono from the 1 cited source below, including Japanese-language reporting where cited, then editorially reviewed before publishing.