Comment by paulddraper

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

The proof was not actually a proof at all, because it was unsound (despite Lean admitting the proof).