AI-generated, Lean-verified proof of Collatz conjecture exploits Lean kernel bug

The plot thickens! It seems the researcher who posted the "proof" of the Collatz conjecture was aware of the Lean bug; or maybe he wasn't. He's currently being coy about it and it's hard to say if he's trying to save face or genuinely intended to cause a stir for whatever reason:

https://leanprover.zulipchat.com/#narrow/channel/270676-lean...