[tomstuart]

I wouldn’t defend the idea that it’s “clear”, but the idea is to build a machine that combines the axioms of ZF set theory in all possible ways to generate all possible conclusions, checking each one for contradiction as it goes. If it never generates a contradictory conclusion from those axioms, it’ll run forever.

[ijustlovemath]

This sounds like it relies on the halting problem, or maybe the other way around? Really interesting stuff, been a while since I read about a higher level math topic and been able to sorta kinda understand the "quanta-level" summaries out there

[jtolmar]

The Nth Busy Beaver number lets you solve the halting problem for Turing Machines up to size N.

Only a handful of them are known, for very small N, and they increase incredibly rapidly. For the most common version of the problem (S for 2-symbol machines), they go: 1, 6, 21, 107, some number greater than or equal to 47176870, and some number greater than 10⇈15 (that's up arrow notation on the last one).

[ijustlovemath]

Ooh, are they basically the number of possible turing programs encodable in a state of N?

[readams]

It's the maximum amount of time a Turing machine of size N can run. So if you want to know whether a Turning machine of size N or less will halt, just run it for BB(N) steps. If it hasn't halted by then, it never will.

[stouset]

I think the part that eludes me here is that it's not clear that such a Turing machine could be built from a finite number of states.