This was never about the Collatz conjecture itself. If I understand the original discussion correctly (as of a few days ago, not sure if new stuff has come to light), everybody agreed that that framing was just a flashy gimmick. And some Lean maintainers were unhappy about it, since this framing just added noise to the reproducer; they would have preferred a simple proof of False. Nobody ever thought that the disproof might be real.
A counterexample of the form "X cycles to X after N steps" is easy to check. A counterexample of the form "starting with X we keep going up forever" is hard to check in finite time.
And still that requires X to not be particularly large. It could conceivably be in ballpark of BB(40).
You, sir, have a very different definition of "not particularly large" than I do!
To be fair, BB(40) is smaller than almost all positive integers.
It’s practically zero, in fact.
This feels like saying there are probably hundreds of stars in the universe
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).
No, Lean allows non-constructive proofs so a proof could be like "if the Riemann hypothesis is true the counterexample is 42 otherwise it is the first nontrivial zero" or something like this, and then you don't get a fully closed counterexample.