> by a combination of automated methods and case-by-case cleverness, people managed to find proofs of non-termination for all the non-halting ... machines
So it's very ad-hoc. You study a particular machines's behaviour and formulate hypotheses about how it can keep going on forever and then try to prove them.
Down here at BB(6) you can feel fairly sure the machine doesn't express anything inherently problematic because it's just too simple. But as the parameter goes up, the machines get sophisticated and very quickly the machines express ideas like "Look at all the positive multiples of seven in turn, halt when Fermat's conjecture is wrong for this value of n" and in that particular case we know the answer is "This never halts" but even thirty years ago the best we can say is "Probably not?".
You only need one "Probably?" or "Probably not?" to be screwed, now you can't even figure out if this machine is a candidate or not.
> Down here at BB(6) you can feel fairly sure the machine doesn't express anything inherently problematic because it's just too simple.
One of the shocking results of Busy Beaver research is that this is actually false. Even with as few as four states there are machines that are complicated and difficult to understand. Turing machine "states" are really GOTO targets, and with six states it's possible to create control flow that is beyond incomprehensible.
Perhaps it means that there is some kind of new and useful (or, interesting at least) generic control flow primitive waiting to be discovered there-- and with it the control flow is again 'simple'. :)
This is really mind boggingly, meaning that there is an actual discrete valicable limit of what can be determined and what can't. Turing machine with 4 states? Cool. Turing machine with 5 states? Sorry, it goes beyond ZFC maths!
The big numbers don't impress me, but the fact that such tiny machines can correspond to complex and even meaningful theorems is fascinating. I wonder what the smallest number of states you need to encode a pre-existing well-known mathematical conjecture is.
They've found a 43-state machine that encodes the Goldbach Conjecture, and proposed but not verified that it can be compressed 27 states. I would consider the Goldbach Conjecture to be "well-known" as far as math theorems go, since it was referenced on Futurama.
> by a combination of automated methods and case-by-case cleverness, people managed to find proofs of non-termination for all the non-halting ... machines
So it's very ad-hoc. You study a particular machines's behaviour and formulate hypotheses about how it can keep going on forever and then try to prove them.
[1] https://scottaaronson.blog/?p=6673#comment-1942654