AI-Assisted Collatz Disproof Invalidated by Lean Kernel Bug
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.