Skelet: Difference between revisions

Revision as of 01:59, 21 May 2025

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.^[1] 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^[2]	TABLE_BASED_SPORADIC
2	`1LC0RE_---0RC_1RD0LA_1RA1RD_1LA0RB` (bbch)	Translated cycler^[3]	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^[3]	TABLE_BASED_NG_3_6
6	`1LC0RB_---0RD_1LD0RA_1RE0LC_1RC1RE` (bbch)	Translated cycler^[3]	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^[4]	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^[3]	TABLE_BASED_Lp1
15	`1LB---_1LC1RB_1RD1LE_1RB0RD_1LA0LC` (bbch)	Shift overflow counter^[5]	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^[3]	TABLE_BASED_RWL_19_2
19	`1LB---_0LC0LB_1RC0RD_1LA0RE_0RA0RE` (bbch)		TABLE_BASED_DNV_10
20	`1LB---_0LC1LD_0RD1LC_1RE0LA_1LA0RE` (bbch)	Bouncer^[6]	TABLE_BASED_RWL_20_2
21	`1LC1LE_1LA---_1RD0RE_1RB1RE_1RC0LA` (bbch)	Bouncer^[6]	TABLE_BASED_RWL_10_3
22	`1LC0LE_1RA---_1RD0LA_0RD1RB_0LC0RB` (bbch)	Translated cycler^[3]	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^[3]	NGRAM_CPS_IMPL1_params_2_2_2_1600
26	`1LC1RE_1RD---_1LD0LC_1RA1LD_1RB0RA` (bbch)	Shift overflow counter^[5]	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^[6]	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^[5]	TABLE_BASED_SPORADIC
34	`1LC1RD_1RE---_0LD0LC_1RB0RA_1RA1LA` (bbch)	Shift overflow counter^[5]	TABLE_BASED_SPORADIC
35	`1LC1RD_1RE---_0LD0LC_1RB0RA_1RA0RA` (bbch)	Shift overflow counter^[5]	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^[6]	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). While Skelet #1 is technically a Translated Cycler, it requires specialized acceleration to prove this. Whereas all the other cyclers can be demonstrated by direction simulation.

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

References

↑ "Story" (section "Skelet's 43 undecided machines").
↑ https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
↑ ^3.0 ^3.1 ^3.2 ^3.3 ^3.4 ^3.5 ^3.6 https://discuss.bbchallenge.org/t/skelet-machines-that-are-translated-cyclers/58
↑ https://www.sligocki.com/2023/03/14/skelet-10.html
↑ ^5.0 ^5.1 ^5.2 ^5.3 ^5.4 https://www.sligocki.com/2023/02/05/shift-overflow.html
↑ ^6.0 ^6.1 ^6.2 ^6.3 https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141

[1] "Story" (section "Skelet's 43 undecided machines").

[2] ttps://www.sligocki.com/2023/03/13/skelet-1-infinite.html

[tc-3] 3.0 ^3.1 ^3.2 ^3.3 ^3.4 ^3.5 ^3.6 https://discuss.bbchallenge.org/t/skelet-machines-that-are-translated-cyclers/58

[4] ttps://www.sligocki.com/2023/03/14/skelet-10.html

[so-5] 5.0 ^5.1 ^5.2 ^5.3 ^5.4 https://www.sligocki.com/2023/02/05/shift-overflow.html

[ctl-6] 6.0 ^6.1 ^6.2 ^6.3 https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141

[1]

[2]

[3]

[4]

[5]

[6]

@@ Line 232: / Line 232: @@
 |
 |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). While Skelet #1 is technically a Translated Cycler, it requires specialized acceleration to prove this. Whereas all the other cyclers can be demonstrated by direction simulation.
+{| class="wikitable sortable"
+!Skelet #
+!Start Step
+!Period
+!Offset
+|-
+|  1 || <math>\approx 5.42 \times 10^{51}</math> || 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
 |}