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).
More details and explanations at:
Keep this in mind when someone claims that requiring formal proofs in Lean is the end-all solution to AI slop and hallucination in mathematical proofs.
(There are other — more frequent — problems, of course, like the fact that the formally proven theorem might not match the informally understood one. Or, more basically, that the proof might be unreadable for humans, making it useless.)
* 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.
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.