An AI-Generated Lean Proof of Collatz Passed Two Kernels by Hitting Two Separate Soundness Bugs — Leo de Moura: 'This Is Going to Keep Happening'
leanprover/lean4 (via Gro-Tsen and Machine Learning Street Talk quoting Leo de Moura)·high signal
An AI-generated formal Lean proof of the Collatz conjecture verified successfully — because it was exploiting a kernel soundness bug (leanprover/lean4 issue #14576: the kernel accepted wrong-structure projections, enabling an axiom-free proof of False with `#print axioms` reporting nothing). It cleared both Lean's official kernel and the independent Nanoda checker by hitting two distinct bugs; both are now patched via PR #14577. Lean creator Leo de Moura's comment is the headline for anyone treating formal verification as an AI-proof oracle: 'This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels.'