[gd1]

Very good point. There's no reason to think we can solve the Halting Problem any more than a TM can, so the 'solved' BBs mentioned in the article are only solved in the sense that we puny humans had a look at all possible programs generated by BB(3) for example, focused on the ones that didn't appear to be halting, and decided by inspection that they wouldn't halt. That inspection process is not mathematically well-defined, so I'd argue that BB numbers should be inadmissible for the contest.

[jerf]

The inspection can include proofs that the loopers loop, with the full mathematical power of the word "proof" behind it, so I'm willing to trust the known numbers. But the proofs can not be general (or at least not past a certain point which probably comes up pretty quickly), and will get ever more difficult to perform as we dig ever further down the sequence.