BB(2,4): Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
(Added a section, "Current Work", and moved my recent additions there.)
m (Fixed link to "Champions")
 
(14 intermediate revisions by 4 users not shown)
Line 1: Line 1:
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 [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in February 2005.
The 2-state, 4-symbol Busy Beaver problem, '''BB(2,4)''', obtained a lower bound of BB(2,4) 3,932,964 when the winner was found in February 2005.  


On August 22, 2024, BB(2,4) = 3,932,964 was officially confirmed by the [[bbchallenge.org]] massively collaborative research project, when a proof for the BB(2,4) case was added to [[Coq-BB5]] and successfully compiled.


== History ==
== History ==
* Brady found a steps and ones champion in 1988, establishing S(2,4) ≥ 7195 and Σ(2,4) ≥ 90.<ref>Brady A.H. (1988) The busy beaver game and the meaning of life in: The Universal Turing Machine: A Half-Century Survey, R. Herken (Ed.), Oxford University Press, 1988, 259-277.</ref>
* Brady found a steps and ones champion in 1988, establishing S(2,4) ≥ 7195 and Σ(2,4) ≥ 90.<ref>Brady A.H. (1988) The busy beaver game and the meaning of life in: The Universal Turing Machine: A Half-Century Survey, R. Herken (Ed.), Oxford University Press, 1988, 259-277.</ref>
* Terry and Shawn Ligocki found the current champion in 2005.
* [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] found the champion in 2005 but they did not prove it was BB(2,4).
 
== Current Work ==
Work formalizing this result is ongoing. 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 tot better capture 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.
 
{| class="wikitable"
|- style="text-align:center;"
| colspan=5|Number of TMs || rowspan=3|Command Used
|- style="text-align:center;"
| rowspan=2|Input || colspan=4|Output
|- style="text-align:center;" 
| Total || Halt || Infinite || Unknown
|- style="text-align:right;"
|      1 || 348,261 || 116,844 || 205,066 || 26,351 || style="text-align:left;"|lr_enum 2 4 1000 BB2x4.halt.txt BB2x4.inf.txt BB2x4.unk.txt false
|- style="text-align:right;"
|  26,351 ||  26,351 ||      0 ||  10,136 || 16,215 || style="text-align:left;"|Reverse_Engineer_Filter.py
|- style="text-align:right;"
|  16,215 ||  16,215 ||      0 ||  13,138 ||  3,072 || style="text-align:left;"|Enumerate.py --block-size=2 --max-loops=1_000 --lin-steps=0 --no-ctl --no-reverse-engineer
|- style="text-align:right;"
|  3,072 ||  3,072 ||      0 ||  2,982 ||    90 || style="text-align:left;"|CPS_Filter.py --min-block-size=1 --max-block-size=6
|- style="text-align:right;"
|      90 ||      90 ||      0 ||      15 ||    75 || style="text-align:left;"|Enumerate.py --max-loops=10_000 --lin-steps=0 --no-ctl --no-reverse-engineer
|- style="text-align:right;"
|      75 ||      75 ||      0 ||      31 ||    44 || style="text-align:left;"|CTL_Filter.py --type=CTL2 --max-block-size=6 --all-offsets
|- style="text-align:right;"
|      44 ||      44 ||      0 ||      13 ||    31 || style="text-align:left;"|Enumerate.py --recursive --max-loops=10_000 --lin-steps=0 --no-ctl --no-reverse-engineer
|- style="text-align:right;"
|      31 ||      31 ||      0 ||      18 ||    13 || style="text-align:left;"|Enumerate.py --recursive --max-loops=10_000 --block-size=2 --lin-steps=0 --no-ctl --no-reverse-engineer
|- style="text-align:right;"
|      13 ||      13 ||      0 ||      1 ||    12 || style="text-align:left;"|Enumerate.py --recursive --max-loops=10_000 --block-size=3 --lin-steps=0 --no-ctl --no-reverse-engineer
|- style="text-align:right;"
|      12 ||      12 ||      0 ||      12 ||      0 || style="text-align:left;"|MITMWFAR -n=14
|-
 
|}


== Champion ==
== Champion ==
S(2,4) = 3,932,964 and Σ(2,4) = 2050 and both are achieved by only one champion (in [[TNF]]):
S(2,4) = 3,932,964 and Σ(2,4) = 2050 and both are achieved by only one [[Champions#4-Symbol TMs|champion]] (in [[TNF]]):
* {{TM|1RB2LA1RA1RA_1LB1LA3RB1RZ|halt}}
* {{TM|1RB2LA1RA1RA_1LB1LA3RB1RZ|halt}}


== Enumeration ==
== Top Halters ==
The top 20 longest running BB(2,4) TMs (in [[TNF-1RB]]) are:
The top 20 longest running BB(2,4) TMs (in [[TNF-1RB]]) are:
Standard Format          Steps  Σ
<pre>
1RB2LA1RA1RA_1LB1LA3RB1RZ 3932964 2050
Standard Format          Status Steps  Σ
1RB3LA1LA1RA_2LA1RZ3RA3RB    7195  90
1RB2LA1RA1RA_1LB1LA3RB1RZ Halt  3932964 2050
1RB3LA1LA1RA_2LA1RZ3LA3RB    6445  84
1RB3LA1LA1RA_2LA1RZ3RA3RB Halt  7195   90
1RB3LA1LA1RA_2LA1RZ2RA3RB    6445  84
1RB3LA1LA1RA_2LA1RZ3LA3RB Halt  6445   84
1RB2RB3LA2RA_1LA3RB1RZ1LB    2351  60
1RB3LA1LA1RA_2LA1RZ2RA3RB Halt  6445   84
1RB3RA1LA2RB_2LA3LA1RZ1RA    1021  53
1RB2RB3LA2RA_1LA3RB1RZ1LB Halt  2351   60
1RB3LA1RZ0RB_2LB2LA0LA0RA    1001  26
1RB3RA1LA2RB_2LA3LA1RZ1RA Halt  1021   53
1RB2LA1RZ3LA_2LA2RB3RB2LB    770  30
1RB3LA1RZ0RB_2LB2LA0LA0RA Halt  1001   26
1RB2LB1RZ3LA_2LA2RB3RB2LB    708  29
1RB2LA1RZ3LA_2LA2RB3RB2LB Halt  770     30
1RB2LA0RB1LB_1LA3RA1RA1RZ    592  24
1RB2LB1RZ3LA_2LA2RB3RB2LB Halt  708     29
1RB3LA3RA0LA_2LB1LA1RZ2RA    392  20
1RB2LA0RB1LB_1LA3RA1RA1RZ Halt  592     24
1RB3LA1LA1RA_2LA1RZ2RB3RB    376  21
1RB3LA3RA0LA_2LB1LA1RZ2RA Halt  392     20
1RB3LA1LA1RA_2LA1RZ0LA3RB    376  21
1RB3LA1LA1RA_2LA1RZ2RB3RB Halt  376     21
1RB3LA3RB0LA_2LA1RZ1LB3RA    374  22
1RB3LA1LA1RA_2LA1RZ0LA3RB Halt  376     21
1RB1RA1LB0RA_2LA3RB2RA1RZ    335  18
1RB3LA3RB0LA_2LA1RZ1LB3RA Halt  374     22
1RB2LA3LA1LB_2LA1RZ2RB0RA    292  18
1RB1RA1LB0RA_2LA3RB2RA1RZ Halt  335     18
1RB0RB1RZ0LA_2LA3RA3LA1LB    289  13
1RB2LA3LA1LB_2LA1RZ2RB0RA Halt  292     18
1RB1LA1RZ0LB_2LA3RB1RB2RA    283  18
1RB0RB1RZ0LA_2LA3RA3LA1LB Halt  289     13
1RB3LA3RA0LA_2LB1LA1RZ3RA    266  19
1RB1LA1RZ0LB_2LA3RB1RB2RA Halt  283     18
1RB2RB1RZ1LB_2LA2LB3RB0RB    241  15
1RB3LA3RA0LA_2LB1LA1RZ3RA Halt  266     19
1RB2RB1RZ1LB_2LA2LB3RB0RB Halt  241     15
</pre>


For the top 100 halting BB(2,4) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/2x4.txt
For the top 100 halting BB(2,4) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/2x4.txt
== References ==
<references/>
[[Category:BB Domains]]

Latest revision as of 11:04, 11 August 2025

The 2-state, 4-symbol Busy Beaver problem, BB(2,4), obtained a lower bound of BB(2,4) ≥ 3,932,964 when the winner was found in February 2005.

On August 22, 2024, BB(2,4) = 3,932,964 was officially confirmed by the bbchallenge.org massively collaborative research project, when a proof for the BB(2,4) case was added to Coq-BB5 and successfully compiled.

History

  • Brady found a steps and ones champion in 1988, establishing S(2,4) ≥ 7195 and Σ(2,4) ≥ 90.[1]
  • Terry and Shawn Ligocki found the champion in 2005 but they did not prove it was BB(2,4).

Champion

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

  • 1RB2LA1RA1RA_1LB1LA3RB1RZ (bbch)

Top Halters

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

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

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

References

  1. Brady A.H. (1988) The busy beaver game and the meaning of life in: The Universal Turing Machine: A Half-Century Survey, R. Herken (Ed.), Oxford University Press, 1988, 259-277.