This had nothing to do with Collatz itself and everything to do with a Lean bug.

The proof was not a proof because it was not sound, even though Lean admitted the proof.