AI Proof of Collatz Conjecture Invalidated by Lean Bug

A Lean formal proof claiming to disprove the Collatz conjecture, aided by AI, has been confirmed invalid. The conjecture, proposed by German mathematician Lothar Collatz in 1937, states that any positive integer eventually reaches 1 under a specific iteration, and remains unproven. Formal verification expert Ramana Kumar posted a project on GitHub on July 25, claiming AI refuted the conjecture, but offered no counterexample, only proving "a number that cannot reach 1."

Kumar later found the method could make Lean accept "False" unconditionally, indicating a bug. Researcher Kiran Gopinathan reduced the issue to a small reproduction and reported it to the Lean team on July 28. The flaw was in the kernel's handling of "nested inductive types," which sometimes ignored "ghost type parameters," letting erroneous parameters pass. Lean developer Leonardo de Moura confirmed the issue, and the team created a fix within an hour, releasing Lean 4.32.2 on July 28.