Lean 4 Bug Found Incidentally by AI, "Proving" Collatz

An AI-generated formal proof in Lean claiming to solve the Collatz problem was found to exploit a bug in the Lean kernel, allowing any statement to be proven. The proof's author was aware of the soundness bug and used Collatz as a demonstration, not a serious solution.

So, someone came up with an AI-generated formal proof, in Lean, of a solution to the Collatz problem, and it turned out that the “proof” was merely exploiting a bug in the Lean kernel allowing you to prove anything . - Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem.Replying to @gro tsen https://x.com/gro tsen I think they just use collatz as a fun way to demonstrate the lean soundness bug. There is a history of this in the theorem proving community. The author knew it was a soundness bug and it was intentional. - I think they just use collatz as a fun way to demonstrate the lean soundness bug. There is a history of this in the theorem proving community. The author knew it was a soundness bug and it was intentional. Join the conversation