Skelet

Georgi Ivanov Georgiev (aka Skelet) was a Busy Beaver hunter who attempted to prove BB(5) in the early 2000s.

bbfind

In 2003, he announced his results on his webpage in which he shared his code bbfind (a 6000 line Pascal program) which he claimed enumerated 150M 5-state TMs and reduced them down to 164 holdouts (he called them "nonregular machines"). After manually analyzing these 164 nonregular machines he reduced it to 43 holdouts which he called "hardly nonregular" (HNR) which were not solvable by his program nor by hand. These 43 HNR TMs became famous examples of hard TMs to prove and these TMs began to be named by their place on this list (such as Skelet 1 and Skelet 17).

Due to the length and lack of comments in bbfind's source code, Skelet's work is not believed to have been independently verified. It is now known that all 43 of these holdouts do not halt. Other work done in bbfind includes computing the correct value of BB(4) and for "RTM(5)" (the set of all "Reversal Turing Machines").

Skelet's 43 HNR TMs

• Skelet's original list: https://skelet.ludost.net/bb/nreg.html
• bbchallenge.org list: https://bbchallenge.org/skelet (canonically numbers the TMs)
• More info on some of Skelet's 43 TMs: https://discuss.bbchallenge.org/t/proving-bb-5-in-coq/225/6

Skelet #	Skelet machine code	Zoology	Proof by Coq-BB5
1	1LC1LE_---1LD_1RD0LD_1LA1RE_0LB0RC (bbch)	Translated cycler	TABLE_BASED_SPORADIC
2	1LC0RE_---0RC_1RD0LA_1RA1RD_1LA0RB (bbch)	Translated cycler	TABLE_BASED_NG_3_6
3	1LC0RA_---1LE_1RD0LB_1RA1RC_0LC1LD (bbch)		TABLE_BASED_NG_3_6
4	1LC0RD_---0LE_1RD1LC_1LE1RA_1LB0LD (bbch)		TABLE_BASED_NG_3_2
5	1LC1LA_---0LD_1RD0LE_1LA0RC_1RC0LB (bbch)	Translated cycler	TABLE_BASED_NG_3_6
6	1LC0RB_---0RD_1LD0RA_1RE0LC_1RC1RE (bbch)	Translated cycler	TABLE_BASED_NG_3_6
7	1LC0RB_---1RE_1LD1LA_1RA0LD_0RA1RC (bbch)		TABLE_BASED_NG_3_6
8	1LC0RB_---0RC_1LD0LC_0RE1LC_0RA1RE (bbch)		TABLE_BASED_RWL_15_2
9	1LC1RD_---0LC_1RA1LC_1RE0RA_1LB0LE (bbch)		TABLE_BASED_DNV_12
10	1LC0LA_---0LC_0RD1LA_1LB1RE_1RD0RE (bbch)	Double Fibonacci counter	TABLE_BASED_SPORADIC
11	1LC0LA_---0RA_0RD1LA_0RE1RD_1LA0RB (bbch)		TABLE_BASED_RWL_15_2
12	1LC0LE_---1LE_0RD1LA_0LA1RC_1RC0LB (bbch)		NGRAM_CPS_IMPL1_params_6_2_2_3200
13	1LC0RB_---1RA_0LD1RE_0RE1LC_1RC0RA (bbch)		NGRAM_CPS_IMPL1_params_6_2_2_3200
14	1LB---_1RC0RE_1LD0RB_0LD1LA_0RC0LA (bbch)	Translated cycler	TABLE_BASED_Lp1
15	1LB---_1LC1RB_1RD1LE_1RB0RD_1LA0LC (bbch)	Shift overflow counter	TABLE_BASED_SPORADIC
16	1LB---_0RC1LD_1RD1RC_1LE0LE_0LA0RB (bbch)		TABLE_BASED_DNV_11
17	1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA (bbch)	Dekaheptoid	TABLE_BASED_SPORADIC
18	1LB---_0LC0RD_1LD0RE_1LE0LA_1RC0RD (bbch)	Translated cycler	TABLE_BASED_RWL_19_2
19	1LB---_0LC0LB_1RC0RD_1LA0RE_0RA0RE (bbch)		TABLE_BASED_DNV_10
20	1LB---_0LC1LD_0RD1LC_1RE0LA_1LA0RE (bbch)	Bouncer	TABLE_BASED_RWL_20_2
21	1LC1LE_1LA---_1RD0RE_1RB1RE_1RC0LA (bbch)	Bouncer	TABLE_BASED_RWL_10_3
22	1LC0LE_1RA---_1RD0LA_0RD1RB_0LC0RB (bbch)	Translated cycler	TABLE_BASED_Lp1
23	1LC0RC_0LD---_1RD0LE_1LC0RE_1RA1LB (bbch)		NGRAM_CPS_IMPL1_params_6_2_2_3200
24	1LC1LA_1RE---_1RD0RD_0RB0LE_0LA1RC (bbch)		TABLE_BASED_DNV_10
25	1LC0RA_1LA---_1RD1LE_1RA0RD_0LE0RB (bbch)	Translated cycler	NGRAM_CPS_IMPL1_params_2_2_2_1600
26	1LC1RE_1RD---_1LD0LC_1RA1LD_1RB0RA (bbch)	Shift overflow counter	TABLE_BASED_SPORADIC
27	1LC0RE_0LE---_1LD0LB_1RA0LA_0RA1RE (bbch)		NGRAM_CPS_IMPL1_params_2_3_3_1600
28	1LC0LE_1RD---_1LB1LE_1RA1RE_1LA0RD (bbch)	Bouncer	TABLE_BASED_RWL_10_3
29	1LC0RD_0LA---_1RA0LD_1RE1LB_1LC0RC (bbch)		NGRAM_CPS_IMPL1_params_6_2_2_3200
30	1LC0LE_1RC---_0RD1LA_1RA0RE_1RB0LE (bbch)		TABLE_BASED_NG_6_11
31	1LC0RB_0RE---_0LD1LC_1LE0LC_1RA0RC (bbch)		TABLE_BASED_RWL_17_2
32	1LC0RE_0LC---_0LD0LB_1RD0RA_1RA1LD (bbch)		NGRAM_CPS_IMPL1_params_2_2_2_1600
33	1LC1RD_1RE---_0LD0LC_1RB0RA_1RA1LE (bbch)	Shift overflow counter	TABLE_BASED_SPORADIC
34	1LC1RD_1RE---_0LD0LC_1RB0RA_1RA1LA (bbch)	Shift overflow counter	TABLE_BASED_SPORADIC
35	1LC1RD_1RE---_0LD0LC_1RB0RA_1RA0RA (bbch)	Shift overflow counter	TABLE_BASED_SPORADIC
36	1LC1RE_1RD---_0LD0LC_1RB1LA_1LD0RA (bbch)		TABLE_BASED_NG_2_2
37	1LC0RB_1RC---_0LD0RD_1RA0LE_1LD1LE (bbch)		NGRAM_CPS_IMPL1_params_2_2_2_1600
38	1LC0LC_1LD---_0LB0RD_0RE1LA_1RA1RE (bbch)		TABLE_BASED_DNV_10
39	1LB1LD_1RC---_1RE1RD_1LE0RC_1LA0LD (bbch)	Bouncer	TABLE_BASED_RWL_10_3
40	1LB0LA_1RC---_0RC0RD_1LE0LB_0LE1LA (bbch)		TABLE_BASED_DNV_3
41	1LB0RA_1LC---_0LD1RE_1LE0LA_1RC0RA (bbch)		TABLE_BASED_NG_6_11
42	1LB0RE_1LC---_0LD0LC_1RD0RA_0RB0RE (bbch)		TABLE_BASED_DNV_9
43	1LB0RA_0LC---_1RC1LD_1LE1RA_0LB0RD (bbch)		TABLE_BASED_NG_7_10

Translated Cycler Periods

Several of Skelet's holdouts were translated cyclers, here are the parameters for them. Start step is the earliest step that the cycle starts at. Period is the step count per cycle. Offset is the translation shift along tape each period (positive to the right, negative to the left).

Skelet #	Start Step	Period	Offset
1	$\approx 5.42\times 10^{51}$	8468569863	-107917
2	15055	4328	74
5	15063	4328	-74
6	24149	4328	74
14	4265	91995	543
18	6102	1143	-19
22	4663	91995	-543
25	6354	589	23

While Skelet #1 is technically a Translated Cycler, it requires specialized acceleration to prove this. Whereas all the other cyclers can be demonstrated by direct simulation.

This list is not necessarily exhaustive, it is possible that some of the other Skelet machines are also Translated Cyclers with very large start step or periods, but were proven infinite using a Closed Set method.