zlacker

I think it is possible, in principle, to find a number which you can be pretty sure is BB(n). The problem I think is being sure that this number really is BB(n).

Like you run all n-state Turing Machines for a super long time, and take the max of the output of all the ones that have halted. Now this might give you BB(n), but you can't be sure because you don't know whether the ones that haven't halted are ever going to halt.

In mathematics, we can just say "Well consider the set of all the ones that do halt, and take their max." In real life, it's not so easy to "consider the set".

>>qmalxp+(OP)
You don't just wait, you prove that they all don't halt. There are only finitely many of them. You can't provide a general algorithm for proving that Turing machines don't halt, each one is going to require a special case - but it will be a fact that the physical instance of the machine halts or doesn't halt. (Or if it halts in some models of ZFC but not others, that would be even more interesting).

>>lmm+8n
There won't always be a proof. If there always was, you could programmatically find it via brute-force search and solve the halting problem.