BB(2,4)

BB(2,4) was unofficially found to be 3,932,964 on April 10, 2023 by the bbchallenge project, when deciders made for solving BB(5) eliminated the last BB(2,4) holdouts. The champion machine M, with S(M) = 3,932,964 and Σ(M) = 2,050, was found by Terry and Shawn Ligocki in February 2005.

History

• Brady found a steps and ones champion in 1988, establishing S(2,4) ≥ 7195 and Σ(2,4) ≥ 90.
• Terry and Shawn Ligocki found the current champion in 2005.

Current Work

Investigations are ongoing to create a minimal Coq proof of this case and to document code run to get the number of holdouts to zero.

A successful proof specifically for BB(2,4) has been added to the Coq-BB5 proof. Although this solves the BB(2,4) problem, investigations are ongoing to make a simpler proof that better captures the complexity of this problem.

One successful attempt to run an existing enumerator and existing deciders is shown in the next table. This is far from minimal but it does reduce the number of unknown TMs to zero. The "Commands Used" needs to be explained more fully. This will happen when the a more minimal set of commands is used.

Number of TMs					Command Used
Input	Output
	Total	Halt	Infinite	Holdouts
1	348,261	116,844	205,066	26,351	lr_enum 2 4 1000 BB2x4.halt.txt BB2x4.inf.txt BB2x4.unk.txt false
26,351	26,351	0	10,136	16,215	Reverse_Engineer_Filter.py
16,215	16,215	0	13,138	3,072	Enumerate.py --block-size=2 --max-loops=1_000 --lin-steps=0 --no-ctl --no-reverse-engineer
3,072	3,072	0	2,982	90	CPS_Filter.py --min-block-size=1 --max-block-size=6
90	90	0	15	75	Enumerate.py --max-loops=10_000 --lin-steps=0 --no-ctl --no-reverse-engineer
75	75	0	31	44	CTL_Filter.py --type=CTL2 --max-block-size=6 --all-offsets
44	44	0	13	31	Enumerate.py --recursive --max-loops=10_000 --lin-steps=0 --no-ctl --no-reverse-engineer
31	31	0	18	13	Enumerate.py --recursive --max-loops=10_000 --block-size=2 --lin-steps=0 --no-ctl --no-reverse-engineer
13	13	0	1	12	Enumerate.py --recursive --max-loops=10_000 --block-size=3 --lin-steps=0 --no-ctl --no-reverse-engineer
12	12	0	12	0	MITMWFAR -n=14
Totals	N/A	116,849	231,412	N/A	N/A

Champion

S(2,4) = 3,932,964 and Σ(2,4) = 2050 and both are achieved by only one champion (in TNF):

• 1RB2LA1RA1RA_1LB1LA3RB1RZ (bbch)

Enumeration

The top 20 longest running BB(2,4) TMs (in TNF-1RB) are:

Standard Format           Steps   Σ
1RB2LA1RA1RA_1LB1LA3RB1RZ 3932964 2050
1RB3LA1LA1RA_2LA1RZ3RA3RB    7195   90
1RB3LA1LA1RA_2LA1RZ3LA3RB    6445   84
1RB3LA1LA1RA_2LA1RZ2RA3RB    6445   84
1RB2RB3LA2RA_1LA3RB1RZ1LB    2351   60
1RB3RA1LA2RB_2LA3LA1RZ1RA    1021   53
1RB3LA1RZ0RB_2LB2LA0LA0RA    1001   26
1RB2LA1RZ3LA_2LA2RB3RB2LB     770   30
1RB2LB1RZ3LA_2LA2RB3RB2LB     708   29
1RB2LA0RB1LB_1LA3RA1RA1RZ     592   24
1RB3LA3RA0LA_2LB1LA1RZ2RA     392   20
1RB3LA1LA1RA_2LA1RZ2RB3RB     376   21
1RB3LA1LA1RA_2LA1RZ0LA3RB     376   21
1RB3LA3RB0LA_2LA1RZ1LB3RA     374   22
1RB1RA1LB0RA_2LA3RB2RA1RZ     335   18
1RB2LA3LA1LB_2LA1RZ2RB0RA     292   18
1RB0RB1RZ0LA_2LA3RA3LA1LB     289   13
1RB1LA1RZ0LB_2LA3RB1RB2RA     283   18
1RB3LA3RA0LA_2LB1LA1RZ3RA     266   19
1RB2RB1RZ1LB_2LA2LB3RB0RB     241   15

For the top 100 halting BB(2,4) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/2x4.txt