Skelet #34 Is Infinite
sligocki.com
sligocki.com
the busy beaver game consists of designing a halting Turing machine with alphabet {0,1} which writes the most 1s on the tape, using only a given set of states. The rules for the 2-state game are as follows:
the machine must have two states in addition to the halting state, and the tape initially contains 0s only.
A player should conceive a transition table aiming for the longest output of 1s on the tape while making sure the machine will halt eventually.
The goal of the Busy Beaver Challenge (bbchallenge for short) is to collaboratively prove or disprove the following conjecture [Aaronson, 2020]: BB(5) = 47,176,870
This conjecture says that 47,176,870 is the maximum number of steps that a 5-state Turing machine can run before halting (starting from all-0 memory tape).
The conjecture is based on earlier work [Marxen and Buntrock, 1990] which discovered the current 5-state busy beaver champion, a machine with 5 states that halts after 47,176,870 steps: 0 1 A 1RB 1LC B 1RC 1RB C 1RD 0LE D 1LA 1LD E --- 0LA
Achieving the goal of the Busy Beaver Challenge implies to study 88,664,064 Turing machines and decide whether they halt or not, see Method.
...
Apparently, there was a single person[1] (Skelet) who had a 6000 line uncommented pascal program that proved all of the trillions of turing machines of 5 states but 164 of them, some 43 of them which were "hard." Of these, yet another author[2] has manually proved 22 of them, leaving 21 of them unproven. Finally, OP proves one of the remaining 21 of them to be infinite, and thus not a candidate for either fitting Aaronson's conjecture or pushing past it. That leaves 20.
Of course, a lot of this hinges on trusting Skelet's results from his computer program, which reading around not everyone does.
[0] https://bbchallenge.org/story#goal
In addition to proving this one machine by hand (which may be necessary to completely prove the BB(5) value), this post also introduces a new type of proof that a TM does not halt (specifically the "Reset Invariant"). There's potential that this technique could be automated to prove a whole group of TMs non-halting (which is the main way that we have made progress on proving Busy Beaver values in the past).