The AI-assisted “disproof of the Collatz conjecture” is invalid, found to have exploited a Lean kernel bug

An AI-assisted Lean proof claiming to disprove the Collatz conjecture was accepted, but it turned out to rely on a Lean kernel type-checking bug and an older Nanoda bug, so the proof was invalid.

The issue highlights a core risk in formal verification: even machine-generated proofs can pass if the proof assistant’s underlying implementation is flawed.

Lean maintainers released Lean 4.32.2 with fixes, tighter checks, and more tests to prevent similar false proofs.