[tcai]

I have some issue with how you're generating the BB numbers, though it's not necessarily mathematical. Fundamentally, "cranking it out" is exactly what you cannot do to generate the BBs: following any one specific set of instructions for generating the BBs is a futile exercise.

The problem arises when you say that "a programmer should be able to grind out" whether or not a TM halts or not, which you use to get around the fact that a TM cannot solve the halting problem. However, I'd question if this is a trivial exercise: while we certainly are capable of recognizing infinite loops in the code we write, I'm not certain that humans can identify arbitrary infinite loops. Obviously, whether or not we can isn't a trivially answerable question, as it comes down to whether or not our brain's neural networks can be modeled by a sufficiently large TM, and even if it cannot be modeled by a sufficiently large TM, what differences between our brains and a TM exist and why those would effectively allow us to solve the halting problem.

So I'd question whether finding the BBs is "'just' a matter of computation", because I'm not convinced that humans can solve the TM halting problem.

[dTal]

I'd say that it is a trivially answerable question - "no, we cannot recognize arbitrary infinite loops" is the answer. It is easy to encode difficult-to-prove statements about number theory into loops. Consider a program that searched for a counterexample to the Collatz conjecture, or the Riemann Hypothesis.

[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.

[tempestn]

Thank you; this is a better explanation of what I was getting at in the GP comment. While it is theoretically possible that we could conclusively find BB(X) for any X, we don't know, nor can we prove, that we can (aside from the ones that have already been proven). Therefore I don't know that it makes sense to talk about it being a specific number, but rather the concept of a number (more like his "number of grains of sand in the Sahara" example, which he explicitly mentioned is not valid^.)

^Although his reasoning is that it is not valid because it is always changing, not specifically because it is unknown. Still, I assume that "Number of grains of sand in the Sahara at exactly midnight, Jan. 1 2050, on this atomic clock" would also be disallowed, even though it's possible we would somehow be able to know exactly what that number is in the future.