> Anyway, the point is that the halting procedure in its full generality cannot exist, while each individual busy beaver number can be solved in theory (even if

> Anyway, the point is that the halting procedure in its full generality cannot exist, while each individual busy beaver number can be solved in theory (even if there’s no algorithm that can list them all). It's possible to prove the values of certain busy beaver numbers, of course, but that's equivalent to noting that you can prove whether certain TMs halt. For example, it is possible to run every n-state TM long enough that, for each TM, you've either observed it halt or you've proved that it's in an infinite loop. The problem is that, for any TM that you haven't observed halt and you haven't been able to prove it's in an infinite loop, you just gotta keep waiting until one or the other happens. And, critically, you can't know if you'll ever come up with a proof that it's in an infinite loop.