BusyBeaverWiki - User contributions [en]

BB(5)

2025-06-25T00:35:36Z

Fr tho: more specific date

The 5-state, 2-symbol Busy Beaver problem, '''BB(5)''', refers to the 5th value of the [[Busy Beaver function]]. In September 1989, the [[5-state busy beaver winner]] was found: a 5-state [[Turing machine]] halting after 47,176,870 steps giving the lower bound BB(5) ≥ 47,176,870.<ref name=":0">H. Marxen and J. Buntrock. Attacking the Busy Beaver 5. Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html</ref>

In 2024, BB(5) = 47,176,870 was proven by the [[bbchallenge.org]] massively collaborative research project.

== History ==
In this Section, we use Radó's original S (number of steps) and Σ (number of ones on the final tape) notations, see [[Busy Beaver Functions]].

=== Finding the 5-state winner ===

* In 1964, Green establishes Σ(5) ≥ 17.<ref name=":1">Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52 </ref>
* In 1972, Lynn establishes S(5) ≥ 435 and Σ(5) ≥ 22.<ref name=":1" />
* In 1973, Weimann establishes S(5) ≥ 556 and Σ(5) ≥ 40.<ref name=":1" />
* In 1974, Lynn, cited by Brady (1983)<ref>Brady, A.H. (1983). The determination of the value of Rado’s noncomputable function Σ() for four-state Turing machines. ''Mathematics of Computation, 40'', 647-665.</ref>, establishes S(5) ≥ 7,707 and Σ(5) ≥ 112.
* In 1983, the [https://docs.bbchallenge.org/other/lud20.pdf Dortmund contest]is organised to find new 5-state champions, winner is Uwe Schult who established S(5) ≥ 134,467 and Σ(5) ≥ 501.
* In 1984, George Uhing establishes S(5) ≥ 2,133,492 and Σ(5) ≥ 1,915.<ref>https://docs.bbchallenge.org/other/busy.html</ref>
* In 1989, Heiner and Buntrock find the [[5-state busy beaver winner]], establishing S(5) ≥ 47,176,870 and Σ(5) ≥ 4,098.<ref name=":0" /> They do not prove (or claim) that the machine is the actual winner (i.e. that no other 5-state machines halt after more steps) but they present some ideas for automatically deciding the behavior of Turing machines (i.e. making [[Deciders]]).<ref name=":0" />

=== Proving that the 5-state winner is actually the winner ===
No machine halting in more steps than the [[5-state busy beaver winner]] has been found since 1989, hinting that it is actually the 5-state winner (i.e. no 5-state machine could halt after more steps). In 2020, Scott Aaronson formally conjectured that BB(5) = 47,176,870.<ref>Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. <nowiki>https://doi.org/10.1145/3427361.3427369</nowiki></ref> In practice, proving this conjecture requires to study the behavior of ~100 million 5-state machines.<ref>https://bbchallenge.org/method</ref>
* In 2003, Georgi Georgiev (Skelet) publishes a list of [[Skelet's 43 holdouts|43 holdouts]], based on [[bbfind]], a collection of [[Deciders]] written in Pascal.<ref>https://skelet.ludost.net/bb/index.html</ref>
* In 2009, Joachim Hertel publishes a method claiming 100 holdouts.<ref>Function, S., & Hertel, J. (2009). Computing the Uncomputable Rado Sigma Function. https://www.mathematica-journal.com/2009/11/23/computing-the-uncomputable-rado-sigma-function/</ref>
* In 2022, [[bbchallenge.org]] is released, with the aim of collaboratively proving that BB(5) = 47,176,870.<ref>https://bbchallenge.org/story</ref>
* In 2024, bbchallenge's contributor @mxdys publishes [[Coq-BB5]], a Coq-verified proof of BB(5) = 47,176,870<ref>https://github.com/ccz181078/Coq-BB5</ref>, ending a 60 years old quest. This proof uses and/or improves on many other bbchallenge's contributions, see [[Coq-BB5]].

== Champions ==
S(5) = 47,176,870 and there is only one shift champion (in [[TNF]]):

* {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} leaves 4098 ones (a ones champion)

Σ(5) = 4098 and there are 2 ones champions (in TNF):

* {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} runs for 47,176,870 steps (the steps champion)
* {{TM|1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC|halt}} runs for 11,798,826 steps

== Top Halters ==
The top 20 longest running BB(5) TMs (in [[TNF-1RB]]) are:
<pre>
Standard format Status S Σ
1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA Halt 47176870 4098
1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt 23554764 4097
1RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ0RB Halt 11821234 4097
1RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ0RB Halt 11821220 4097
1RB1RA_0LC0RC_1RZ1RD_1LE0LA_1LA1LE Halt 11821190 4096
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC0LA Halt 11815076 4096
1RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ1LC Halt 11811040 4097
1RB1RA_1LC1LB_0RC1LD_1RA0LE_1RZ1LC Halt 11811040 4097
1RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ1LC Halt 11811026 4097
1RB1RA_0LC0RC_1RZ1RD_1LE1RB_1LA1LE Halt 11811010 4096
1RB1RA_1LC1LB_1RA1LD_0RE0LE_1RZ1LC Halt 11804940 4097
1RB1RA_1LC1LB_1RA1LD_1RA0LE_1RZ1LC Halt 11804926 4097
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_0LE1RB Halt 11804910 4096
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC1RB Halt 11804896 4096
1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC Halt 11798826 4098
1RB1RA_1LC1RD_1LA1LC_1RZ0RE_1LC1RB Halt 11798796 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_0LE0RB Halt 11792724 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_1LA0RB Halt 11792696 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt 11792682 4097
1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA Halt 2358064 1471
</pre>
For more top halting BB(5) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/5x2

== References ==
<references />
[[Category:BB Domain]]

BB(2,4)

2025-06-25T00:34:37Z

Fr tho: more specific date

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.<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>
* [[User:tjligocki|Terry]] and [[User:sligocki|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]]):
* {{TM|1RB2LA1RA1RA_1LB1LA3RB1RZ|halt}}

== Top Halters ==
The top 20 longest running BB(2,4) TMs (in [[TNF-1RB]]) are:
<pre>
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
</pre>

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 Domain]]

BB(7)

2025-06-25T00:27:45Z

Fr tho: Updated introduction for consistency

The 7-state, 2-symbol Busy Beaver problem, '''BB(7)''', refers to the unsolved 7th value of the [[Busy Beaver function]]. With the compilation of the [[Cryptid]] machine [[Bigfoot]] into a 7-state, 2-symbol machine in May 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(7).

The current BB(7) champion {{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_0RG0RF}} was discovered by Pavel Kropitz in May 2025, proving the lower bound: <math display="block">S(7) > \Sigma(7) > 2 \uparrow^{11} 2 \uparrow^{11} 3</math>

== History ==
Before 2025, the only known BB(7) champions were produced by hand, not by search. For example, Milton Green designed a machine in 1964 that had [[sigma score]] 22,961 and Wythagoras modified a BB(6) champion in 2014 to produce a machine that had sigma score <math>> 10 \uparrow\uparrow 5</math>.

In May 2025, mxdys shared [https://github.com/ccz181078/TM C++ code] that breaks up the BB(7) enumeration into 1 million subtasks which each run for about 2 minutes and leave ~100 holdouts each. Various folks on Discord have been investigating different sections of this domain to search for champions.

Within three days of the code's release, the Ligockis found three champions after applying their deciders to enumerator output. Shawn Ligocki found the first two, {{TM|1RB0RF_1LC0RE_1RD1LB_1LA1LD_0RA0LE_1RG0LB_1RZ1RB}} and {{TM|1RB1RA_1RC0LC_0LD1LG_1LF0LE_1RZ1LF_0LA1LD_1RA1LC}}, with sigma scores of approximately 10 ↑↑ 22 and 10 ↑↑ 35. That evening, Terry Ligocki found {{TM|1RB0LG_1RC0RF_1LD1RZ_1LF0LE_1RA1LD_1LG1RE_0LB0LB}}, with sigma score ~10 ↑↑ 46. These were all outpaced by Pavel's champion.

Pavel's champion is enumerated in subtask 243308.

== Top Halters ==
Based on limited search through a subset of the 1 million subtasks from mxdys's code, the top 20 scoring known machines are:
{| class="wikitable"
!TM
!Approximate sigma score
!Discoverer
|-
|{{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_0RG0RF}}
|<math>2 \uparrow^{11} 2 \uparrow^{11} 3</math>
|Pavel Kropitz
|-
|{{TM|1RB1RZ_0RC0RE_1LD1LA_1LC0LG_0RF1LF_0RD1LF_1LB0LE}}
|10 ↑↑ 519.20
|Andrew Ducharme
|-
|{{TM|1RB1RF_0RC1RG_1LD1LE_0LE1LD_0RF0LC_1RA0LC_0RF1RZ}}
|10 ↑↑ 286.17
|Terry Ligocki
|-
|{{TM|1RB0LE_1RC0RA_1RD0RC_1LE1LD_1LA0LF_0LA0LG_1RZ0RD}}
|10 ↑↑ 246.32
|@Iijil
|-
|{{TM|1RB0RB_1LC1RG_1RD1RC_1RE0RA_1LF0LB_1RF0LE_0RD1RZ}}
|10 ↑↑ 228.78
|Terry Ligocki
|-
|{{TM|1RB0LD_0LC1RZ_1RA0RD_1RE1LD_1LF0RC_0LG1LE_1RG0LD}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB1LA_1LC0RE_0LD1LB_1RD0LA_1RF0RA_0RG0LA_1RB1RZ}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB1LA_1LC0RE_0LD1LB_1RD0LA_1RF0RA_1RG0LA_0LE1RZ}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB1RZ_1LC0RE_0LD1LB_1RE0LA_1RF0RG_0RA0LG_1RB1LG}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB1RZ_1LC0RE_0LD1LB_1RE0LA_1RF0RG_0RG0LG_1RB1LG}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB1RZ_1LC0RE_0LD1LB_1RE0LG_1RF0RG_0RA0LG_1RB1LG}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB1RZ_1LC0RF_0LD1LB_1RD0LE_1RB1LE_1RG0RE_0RA0LE}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB0LD_0LC1RZ_1RA0RD_1RE1LD_1LF0RC_0LG1LE_1RC0LD}}
|10 ↑↑ 192.67
|Andrew Ducharme
|-
|{{TM|1RB1LA_1LC0RE_0LD1LB_1RE1LG_1RF0LG_0RA0LA_0RF1RZ}}
|10 ↑↑ 192.67
|Andrew Ducharme
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_1LG1RE_1LD0RF_0RA1RE_1RZ0RA}}
|10 ↑↑ 188.28
|@XnoobSpeakable, @Peacemaker II
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_0LG1RE_0RF0LF_0RA1RE_1RZ1LA}}
|10 ↑↑ 188.28
|Terry Ligocki
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_0LG1RE_1LD0RF_0RA1RE_1RZ1LA}}
|10 ↑↑ 188.28
|Terry Ligocki
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_0LG1RE_1LF0RF_0RA1RE_1RZ0RE}}
|10 ↑↑ 188.28
|Terry Ligocki
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_0LG1RE_1LF0RF_0RA1RE_1RZ1LA}}
|10 ↑↑ 188.28
|Terry Ligocki
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_1LG1RE_0RF0LF_0RA1RE_1RZ0LE}}
|10 ↑↑ 188.28
|Terry Ligocki
|}

The top 20 known halters with unique scores are:

{| class="wikitable"
!TM
!Approximate sigma score
!Discoverer
|-
|{{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_0RG0RF}}
|<math>2 \uparrow^{11} 2 \uparrow^{11} 3</math>
|Pavel Kropitz
|-
|{{TM|1RB1RZ_0RC0RE_1LD1LA_1LC0LG_0RF1LF_0RD1LF_1LB0LE}}
|10 ↑↑ 519.20
|Andrew Ducharme
|-
|{{TM|1RB1RF_0RC1RG_1LD1LE_0LE1LD_0RF0LC_1RA0LC_0RF1RZ}}
|10 ↑↑ 286.17
|Terry Ligocki
|-
|{{TM|1RB0LE_1RC0RA_1RD0RC_1LE1LD_1LA0LF_0LA0LG_1RZ0RD}}
|10 ↑↑ 246.32
|@Iijil
|-
|{{TM|1RB0RB_1LC1RG_1RD1RC_1RE0RA_1LF0LB_1RF0LE_0RD1RZ}}
|10 ↑↑ 228.78
|Terry Ligocki
|-
|{{TM|1RB1RZ_1LC0RE_0LD1LB_1RE0LA_1RF0RG_0RA0LG_1RB1LG}}
|10 ↑↑ 192.67
|Terry Ligocki
|-
|{{TM|1RB0LC_1LC1LD_1LA1LB_0LG1RE_1LD0RF_0RA1RE_1RZ1LA}}
|10 ↑↑ 188.28
|Terry Ligocki
|-
|{{TM|1RB0LC_1LC0LD_1LA1LB_0LG1RE_1LD0RF_0RA1RE_1RZ1LC}}
|10 ↑↑ 140.28
|@stokastic
|-
|{{TM|1RB0LG_0RC1RZ_1LD0LA_1RE1LE_1LC1RF_0RE0RA_0RF1LG}}
|10 ↑↑ 133.85
|@poppuncher
|-
|{{TM|1RB1RZ_1RC0RF_1LD1RB_1RG0LE_1LD0RA_1RE0LD_0RC1LF}}
|10 ↑↑ 129.24
|@Iijil
|-
|{{TM|1RB0LC_1RC0RG_1RD0LF_1RE0RF_1LA1RG_1LE1LF_1RZ1RD}}
|10 ↑↑ 126.20
|@stokastic
|-
|{{TM|1RB0LD_1RC1RA_0RD1RG_1LE1LF_0LF1LE_0RA0LD_0RA1RZ}}
|10 ↑↑ 124.86
|Terry Ligocki
|-
|{{TM|1RB1LF_1RC1RA_1LD0LD_1LA1LE_0LA0LD_1LG0RF_0LE1RZ}}
|10 ↑↑ 116.98
|Terry Ligocki
|-
|{{TM|1RB0RD_1RC0LA_0LA0LE_1RE1RZ_1RF0RA_1LG0LE_1LC0LG}}
|10 ↑↑ 116.05
|
|-
|{{TM|1RB0RD_1RC0RA_0RD1LD_0LE1LF_1LA0LG_0LC1LB_1LC1RZ}}
|10 ↑↑ 115.52
|@prurq
|-
|{{TM|1RB0RF_1RC0RB_0RD0RF_1LE0LG_1LC0RD_1LA0LD_1LF1RZ}}
|10 ↑↑ 114.61
|Andrew Ducharme
|-
|{{TM|1RB0RE_1LC0LA_1LD0LC_0LE0LA_1RF0RG_1RD0LE_1RA1RZ}}
|10 ↑↑ 114.60
|Shawn Ligocki
|-
|{{TM|1RB0RE_0RC1LC_0LD1LF_1LE0LG_1RA0RC_0LB1LA_1LB1RZ}}
|10 ↑↑ 114.57
|Andrew Ducharme
|-
|{{TM|1RB0RC_1LC1LD_1RA0RD_0LF1LE_0LB1LA_0RE0LG_1LB1RZ}}
|10 ↑↑ 114.37
|@C7X
|-
|{{TM|1RB0RG_1LC0LE_1LD0LB_1RB1RE_0RA1RF_0RD1RC_1RD1RZ}}
|10 ↑↑ 113.38
|Terry Ligocki
|}

== Current Progress ==
This is a summary of the 1 million subtasks from mxdys's code that have been processed, including further processing by Shawn Ligocki's linear rule code ("TBD" = "To Be Determined", "TBE" = "To Be Entered"):
{| class="wikitable defaultleft"
!rowspan="2"|Task range
!rowspan="2"|Done by
!colspan="2"|Completed
!rowspan="2"|# holdouts
!rowspan="2"|Maximum Score TM
!rowspan="2"|~Sigma
!rowspan="2"|Source
|-
!enumeration
!linear rule
|-
|00xxxx
|rowspan="10"|@Iijil
|Yes
|Yes
|728,495
|{{TM|1RB0RF_1RC1LF_0RD0RD_1LE0LB_1RA1RZ_1LG1RA_1LD0RC}}
|10 ↑↑ 45.64
|rowspan="10"|[https://drive.google.com/drive/folders/1wniwrAuvsHfkvro8Tg65WAMNZEuIekzD Google Drive folder]
|-
|01xxxx
|Yes
|Yes
|817,178
|{{TM|1RB0LE_1RC0RA_1RD0RC_1LE1LD_1LA0LF_0LA0LG_1RZ0RD}}
|10 ↑↑ 246.32
|-
|02xxxx
|Yes
|No
|963,486
|TBD
|TBD
|-
|03xxxx
|Yes
|No
|1,052,504
|TBD
|TBD
|-
|04xxxx
|Yes
|No
|955,711
|TBD
|TBD
|-
|05xxxx
|Yes
|No
|1,056,745
|TBD
|TBD
|-
|06xxxx
|Yes
|No
|950,271
|TBD
|TBD
|-
|07xxxx
|Yes
|No
|1,053,750
|TBD
|TBD
|-
|08xxxx
|Yes
|No
|951,114
|TBD
|TBD
|-
|09xxxx
|Yes
|No
|1,052,362
|TBD
|TBD
|-
|10xxxx
| rowspan="3" |Andrew Ducharme
|Yes
|Yes
|802,059
|{{TM|1RB0LG_1RC0RA_1LD0LE_1LG1LC_1LF0RB_0LC0RC_1LA1RZ}}
|10 ↑↑ 40.79
| rowspan="3" |[https://drive.google.com/drive/folders/16uDjgOahkhAMWv3v-YWmxJG7xxsBvj4h?usp=sharing Google Drive folder]
|-
|11xxxx
|No
|No
|TBD
|TBD
|TBD
|-
|12xxxx
|No
|No
|TBD
|TBD
|TBD
|-
|13xxxx
|Shawn Ligocki
|Yes
|Yes
|1,192,442
|{{TM|1RB0RE_1LC0LA_1LD0LC_0LE0LA_1RF0RG_1RD0LE_1RA1RZ}}
|10 ↑↑ 114.60
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|
20xxxx - 
23xxxx
|@C7X
|Yes
|No
|4,021,883
|TBD
|TBD
|[https://drive.google.com/drive/folders/11iGTKsvu2Y7aFrwOcWS1LYvcN6i_7-JM?usp=sharing Google Drive folder]
|-
|24xxxx
|Andrew Ducharme
|Yes
|Yes
|712,356
|{{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_0RG0RF}}*
|<math>2 \uparrow^{11} 2 \uparrow^{11} 3^*</math>
|[https://drive.google.com/drive/folders/16uDjgOahkhAMWv3v-YWmxJG7xxsBvj4h?usp=sharing Google Drive folder]
|-
|25xxxx
|rowspan="10"|@stokastic
|Yes
|Yes
|815,919
|{{TM|1RB1RZ_1LC0LE_0LD0LC_0RE1LB_1RF0RG_0LD1RB_1RD1RA}}
|10 ↑↑ 31.33
|rowspan="10"|[https://drive.google.com/drive/folders/16_qIdWWD-wolj6zURB5ZSbY-otI4zoUF?usp=sharing Google Drive folder]
|-
|26xxxx
|Yes
|Yes
|731,995
|{{TM|1RB1RZ_0LC1RB_0LE0LD_1LE1LD_0RF0LC_0RG1RF_1RD0RA}}
|10 ↑↑ 36.26
|-
|27xxxx
|Yes
|Yes
|811,486
|{{TM|1RB0RG_1LC1LB_0RE0LD_0LC1RF_0RA1RE_0LF0LB_1RF1RZ}}
|10 ↑↑ 63.56
|-
|28xxxx
|Yes
|Yes
|956,935
|{{TM|1RB1RZ_0LC1RC_0RE1RD_0RB1RG_1RF0RA_1LG0LC_1LB0LF}}
|10 ↑↑ 114.57
|-
|29xxxx
|Yes
|Yes
|1,052,415
|{{TM|1RB1LA_1RC1RD_0LA1LG_1RZ0LE_1RB1RF_1RE0LC_0RE1LF}}
|10 ↑↑ 31.67
|-
|30xxxx
|Yes
|Yes
|1,032,095
|{{TM|1RB0LC_1RC0RG_1RD0LF_1RE0RF_1LA1RG_1LE1LF_1RZ1RD}}
|10 ↑↑ 126.20
|-
|31xxxx
|Yes
|Yes
|1,436,970
|{{TM|1RB1LD_1LC0RF_0RA0LB_0LE1RZ_1LA0LE_1RG1LA_0RC0RF}}
|10 ↑↑ 50.27
|-
|32xxxx
|Yes
|Yes
|1,036,950
|{{TM|1RB1RD_1LC0RF_0LE0LD_1LE1LE_1RF0LB_1RB0RG_1RA1RZ}}
|10 ↑↑ 50.28
|-
|33xxxx
|Yes
|Yes
|1,432,081
|{{TM|1RB0LC_1LC0LD_1LA1LB_0LG1RE_1LD0RF_0RA1RE_1RZ1LC}}
|10 ↑↑ 140.28
|-
|34xxxx
|Yes
|Yes
|1,032,970
|{{TM|1RB0RA_1LC0LE_0LD0LB_1RE0RD_0RA0LF_1RD1RG_0RF1RZ}}
|10 ↑↑ 72.69
|-
|
35xxxx - 
39xxxx
|Terry Ligocki
|Yes
|Yes
|4,894,047
|{{TM|1RB1RZ_1LC0RF_0LD1LB_1RD0LE_1RB1LE_1RG0RE_0RA0LE}}
|10 ↑↑ 192.67
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|40xxxx
| rowspan="8" |Andrew Ducharme
|Yes
|Yes
|730,310
|{{TM|1RB1RZ_0RC0RE_1LD1LA_1LC0LG_0RF1LF_0RD1LF_1LB0LE}}
|10 ↑↑ 519.20
| rowspan="8" |[https://drive.google.com/drive/folders/16uDjgOahkhAMWv3v-YWmxJG7xxsBvj4h?usp=sharing Google Drive folder]
|-
|41xxxx
|Yes
|Yes
|814,075
|{{TM|1RB0LD_0LC1RZ_1RA0RD_1RE1LD_1LF0RC_0LG1LE_1RC0LD}}
|10 ↑↑ 192.67
|-
|42xxxx
|Yes
|Yes
|739,729
|{{TM|1RB1LD_0RC1RF_1LD0LE_0LE0LA_1LA1LE_1RG0LA_1RZ1RA}}
|10 ↑↑ 46.26
|-
|43xxxx
|Yes
|Yes
|817,332
|{{TM|1RB0LE_1RC1RA_1RD0RG_1LA1RZ_1RA1LF_1LA0LE_0RF1RG}}
|10 ↑↑ 93.81
|-
|44xxxx
|Yes
|Yes
|729,686
|{{TM|1RB1LC_1RC0RC_1RD1LA_0RE1RF_1LC0LG_1LA1LE_1RZ1LF}}
|10 ↑↑ 76.36
|-
|45xxxx
|Yes
|Yes
|812,973
|{{TM|1RB0RE_0RC1LC_0LD1LF_1LE0LG_1RA0RC_0LB1LA_1LB1RZ}}
|10 ↑↑ 114.57
|-
|46xxxx
|Yes
|Yes
|725,102
|{{TM|1RB1RA_0LC0RE_0LD1LC_1LA0LF_0RB0RA_1LG1RZ_0RE1LG}}
|10 ↑↑ 36.26
|-
|47xxxx
|Yes
|Yes
|812120
|{{TM|1RB1LA_1LC0RE_0LD1LB_1RE1LG_1RF0LG_0RA0LA_0RF1RZ}}
|10 ↑↑ 192.67
|-
|48xxxx
| rowspan="2" |Tobiáš Brichta
|No
|No
|TBD
|TBD
|TBD
| rowspan="2" |[https://drive.google.com/drive/folders/1-csgJ5uSIX3SKlqTkSnhkUuEYLKgCw81 Google Drive folder]
|-
|49xxxx
|No
|No
|TBD
|TBD
|TBD
|-
|500xxx
|rowspan="2"|@prurq
|Yes
|Yes
|120,520
|{{TM|1RB0RD_1RC0RA_0RD1LD_0LE1LF_1LA0LG_0LC1LB_1LC1RZ}}
|10 ↑↑ 115.52
|rowspan="2"|[https://drive.google.com/drive/folders/145H4sT4F9KJYGSrlIETZdBOIMR7krLQm Google Drive folder]
|-
|501xxx
|Yes
|No
|96,102
|TBD
|TBD
|-
|60xxxx
| rowspan="5" |@gerbil5709
|Yes
|No
|957,769
|TBD
|TBD
| rowspan="5" |[https://drive.google.com/drive/folders/1kAvBebeF09CEVocCk5bGKlDJfRN8co_i?usp=sharing Google Drive folder]
|-
|61xxxx
|Yes
|No
|1,052,047
|TBD
|TBD
|-
|62xxxx
|Yes
|No
|959,753
|TBD
|TBD
|-
|63xxxx
|Yes
|No
|1,051,882
|TBD
|TBD
|-
|64xxxx
|No
|No
|TBD
|TBD
|TBD
|-
|
65xxxx - 
68xxxx
|Terry Ligocki
|Yes
|Yes
|3,076,778
|{{TM|1RB0LD_0LC1RZ_1RA0RD_1RE1LD_1LF0RC_0LG1LE_1RG0LD}}
|10 ↑↑ 192.67
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|69xxxx
|@poppuncher
|Yes
|Yes
|1,053,119
|{{TM|1RB0LG_0RC1RZ_1LD0LA_1RE1LE_1LC1RF_0RE0RA_0RF1LG}}
|10 ↑↑ 133.85
|[https://drive.google.com/drive/folders/1KlCZqXxqVPuBPkDcCBocuMPA8paq9b8P?usp=drive_link Google Drive folder]
|-
|70xxxx
|@hipparcos
|Yes
|Yes
|798,304
|{{TM|1RB0LF_1RC1LE_0RD1RA_1RE1RG_0LA1LB_1LE1RG_0RC1RZ}}
|10 ↑↑ 33.81
|[https://github.com/jhuang97/bb7x2/releases/tag/70xxxx Github release]
|-
|71xxxx
|@hipparcos
|Yes
|Yes
|1,100,790
|{{TM|1RB1RZ_1LC1RD_0LD0LC_1LE1RA_1LF0LE_1RF0RG_1RG0RD}}
|10 ↑↑ 77.50
|[https://github.com/jhuang97/bb7x2/releases/tag/71xxxx Github release]
|-
|72xxxx
|Terry Ligocki
|No
|No
|TBD
|TBD
|TBD
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|73xxxx
|Terry Ligocki
|Yes
|Yes
|1,108,638
|{{TM|1RB0LD_1RC1RA_1LA0RG_1LF0LE_0RF1RE_0LC0LA_0RE1RZ}}
|10 ↑↑ 42.09
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|74xxxx
|Terry Ligocki
|Yes
|Yes
|798,836
|{{TM|1RB1RZ_0LC1RG_1RE1LD_1LC0LG_1LB0RF_1RE0LA_1LF0RE}}
|10 ↑↑ 129.24
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|75xxxx
|Terry Ligocki
|Yes
|Yes
|1,103,089
|{{TM|1RB0LC_1LC1LD_1LA1LB_0LG1RE_0RF0LF_0RA1RE_1RZ1LA}}
|10 ↑↑ 188.28
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|76xxxx
|Terry Ligocki
|Yes
|Yes
|796,008
|{{TM|1RB1LG_1RC0RE_0RD0RB_0LE1RZ_0RF0LB_1LG1LA_0LA0LC}}
|10 ↑↑ 18.61
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|77xxxx
|Terry Ligocki
|Yes
|Yes
|1,105,621
|{{TM|1RB1RF_1LC1LE_0RD1LC_0RB1RE_1RA0LB_1RD0RG_1RZ1RD}}
|10 ↑↑ 42.35
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|78xxxx
|Terry Ligocki
|Yes
|Yes
|800,141
|{{TM|1RB0LD_1RC1RA_0RD1RG_1LE1LF_0LF1LE_0RA0LD_0RA1RZ}}
|10 ↑↑ 124.86
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|79xxxx
|Terry Ligocki
|Yes
|Yes
|1,104,247
|{{TM|1RB0RB_1LC1RG_1RD1RC_1RE0RA_1LF0LB_1RF0LE_0RD1RZ}}
|10 ↑↑ 228.78
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|-
|80xxxx
|@xnoobspeakable
|Yes
|No
|964,396
|TBD
|TBD
| rowspan="2" |[https://drive.google.com/drive/folders/1TpuEC7KottEmvsFnCREugnlVMPaY5ZHi?usp=sharing Google Drive folder]
|-
|81xxxx
|@xnoobspeakable
|No
|No
|TBD
|TBD
|TBD
|-
|
82xxxx - 
99xxxx
|Terry Ligocki
|Yes
|Yes
|15,673,786
|{{TM|1RB1RF_0RC1RG_1LD1LE_0LE1LD_0RF0LC_1RA0LC_0RF1RZ}}
|10 ↑↑ 286.17
|[https://drive.google.com/drive/folders/1_lIqfvj4_J7WWl5LOBUp_pntoI99QYui Google Drive folder]
|}
<nowiki>*</nowiki>The current BB(7) champion TM {{TM|1RB0RA_1LC1LF_1RD0LB_1RA1LE_1RZ0LC_1RG1LD_0RG0RF}}* was discovered by Pavel Kropitz in the enumeration of subtask 243308. The remaining subtasks in the 24xxxx range were enumerated and filtered by Andrew Ducharme.
[[Category:BB Domain]]

BB(3,3)

2025-06-25T00:21:20Z

Fr tho: Update formatting

The 3-state, 3-symbol Busy Beaver problem, '''BB(3,3)''', is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Bigfoot]] in October 2023, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(3,3) and thus [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3,3) is Hard].

The current BB(3,3) champion {{TM|0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC|halt}} was discovered by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in November 2007, proving the lower bounds:

<math display="block">\begin{array}{lcrl}
S(3, 3) & \ge & 119{,}112{,}334{,}170{,}342{,}541 & > 10^{17} \\
\Sigma(3, 3) & \ge & 374{,}676{,}383 & > 10^8 \\
\end{array}</math>

One of the 6 currently unsolved TMs, {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}, is under exploration on Discord and believed to [[probviously]] halt. If it halts, it will be the new champion.

== Cryptids ==
Known Cryptids:
* {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}, known as [[Bigfoot]]
Potential Cryptids:

* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}

== Top Halters ==
The current top 10 BB(3,3) halters (known by [[User:sligocki|Shawn Ligocki]]) are:
<pre>
Standard format Status S Σ
0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC Halt 119112334170342541 374676383
1RB2LA1LC_0LA2RB1LB_1RZ1RA1RC Halt 119112334170342540 374676383
1RB2RC1LA_2LA1RB1RZ_2RB2RA1LC Halt 4345166620336565 95524079
1RB1LA2LC_2LA2RB1RB_1RZ0LB0RC Halt 452196003014837 21264944
1RB1RZ2LC_1LC2RB1LB_1LA2RC2LA Halt 4144465135614 2950149
1RB2LA1RA_1RC2RB0RC_1LA1RZ1LA Halt 987522842126 1525688
1RB1RZ2RB_1LC0LB1RA_1RA2LC1RC Halt 4939345068 107900
1RB2LA1RA_1LB1LA2RC_1RZ1LC2RB Halt 1808669066 43925
1RB2LA1RA_1LC1LA2RC_1RZ1LA2RB Halt 1808669046 43925
1RB2LA1RA_1LB1LA2RC_1RZ1LA2RB Halt 1808669046 43925
</pre>
Numbers listed are step count and sigma score for each TM. For a longer list of halting TMs see https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/3x3. For historical perspective see Pascal Michel's [https://bbchallenge.org/~pascal.michel/ha#tm33 '''Historical survey of Busy Beavers'''].

== Certified Progress ==
On [https://discord.com/channels/960643023006490684/1259770474897080380/1325592156257124443 5 Jan 2025], @tjligocki finished an enumeration and filtering of the BB(3,3) machines using the established Ligocki filters, listing the filter used for each machine. He also computed the number of steps and sigma scores for all found halting TMs. The thorough results are located [https://drive.google.com/drive/folders/101U9htddFdE889agAZnU58VLgQJlfn0v?usp=drive_link here]. 367 machines remained on that list. These results were updated on [https://discord.com/channels/960643023006490684/1259770474897080380/1352398469456859167 20 Mar 2025] in the same location and 76 machines remained on the list.

Over two-thirds of the 367 remaining machines were shown to be non-halting with FAR and MITMWFAR by @Justin Blanchard on [https://discord.com/channels/960643023006490684/1259770474897080380/1262265485639286876 14 July 2024]. Most of the remainders were shown non-halting by @lijil on [https://discord.com/channels/960643023006490684/1084047886494470185/1116351783040716830 8 June 2023.] Together, this leaves 21 unsolved TMs, all of which were on @Justin Blanchard's informal holdouts list of 22 machines (see below). The extra machine on Justin's list {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} had been solved by @lijil before, but this was not realized for some time.

On [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 26 Feb 2025], @mxdys published a list of 19 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @Justin Blanchard's June 2024 informal [[Holdouts lists|holdouts list]] of 22 TMs.

=== Cryptids ===
* {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}} (829), Bigfoot

=== Unsolved ===
* {{TM|1RB1LB2LC_1LA2RB1RB_---0LA2LA|undecided}} (397)
* {{TM|1RB0LB0RC_2LC2LA1RA_1RA1LC---|undecided}} (153, equivalent to 758)
* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}} (758, equivalent to 153)
* {{TM|1RB2LA1LA_2LA0RA2RC_---0LC2RA|undecided}} (531, equivalent to 532), Wily Coyote
* {{TM|1RB2LA1LA_2LA0RA2RC_---1RB2RA|undecided}} (532, equivalent to 531)

=== Solved with moderate rigor ===
* {{TM|1RB2LA1LC_1LA2RB1RB_---2LB0LC|undecided}} (543). See argument for non-halting by @dyuan on [https://discord.com/channels/960643023006490684/1084047886494470185/1240854539519791216 16 May 2024] and [https://discord.com/channels/960643023006490684/1259770474897080380/1325646208483590177 5 January 2025]
* {{TM|1RB1LC1LC_1LA2RB0RB_2LB---0LA|undecided}} (412) ([https://cosearch.bbchallenge.org/contribution/f9gdw0mg cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1279055891559223399 Longitudinal analysis by @Legion implies non-halting]
* {{TM|1RB2LB0LC_2LA2RA1RB_---2LA1LC|undecided}} (650) ([https://cosearch.bbchallenge.org/contribution/32099ui7 cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1290044219481657476 Longitudinal analysis (with extra typo disclaimer) by @Legion implies non-halting]

* {{TM|1RB0RC---_2RC0LB1LB_2LC2RA2RB|undecided}} (279). [https://discord.com/channels/960643023006490684/1084047886494470185/1256729514076016733 Longitudinal analysis by @Legion implies non-halting]
* {{TM|1RB2RB1LC_1LA2RB0RB_2LB---0LA|undecided}} (867). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting]

=== Formally proven ===
* {{TM|1RB1LC---_0LC2RB1LB_2LA0RC1RC|undecided}} (400, equivalent to 494). [https://discord.com/channels/960643023006490684/1218877181321678928/1265131102289264690 Coq proof by @-d]. [https://discord.com/channels/960643023006490684/1084047886494470185/1215532512307052634 Equivalence argument provided by @Legion]

* {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} (494, equivalent to 400, non-halting certified on @lijil's list, equivalence not certified)
* {{TM|1RB2LA2RA_1LC1LB0RA_2RA0LB---|undecided}} (637) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys]. Analyzed by [https://discord.com/channels/960643023006490684/1084047886494470185/1211655096098885732 @Justin], proven by [https://discord.com/channels/960643023006490684/1084047886494470185/1222028527755460700 @dyuan] and [https://discord.com/channels/960643023006490684/1259770474897080380/1327101773604720730 @Andrew]
* {{TM|1RB2LB---_1RC2RB1LC_0LA0RB1LB|undecided}} (642, related to Group 1) ([https://cosearch.bbchallenge.org/contribution/3wxkcx6f cosearch]). Coq proof by @-d. [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan
* {{TM|1RB2RB---_1LC2LB1RC_0RA0LB1RB|undecided}} (834) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys] [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan, who noted a similarity to 642
The following TMs were Coq-decided individually [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 by @mxdys], but analysis beforehand showed their halting problems were highly dependent on that of machine 816. If it was non-halting, then 21, 92, 683, 817, and 818 were all non-halting. If 816 halted via transition C0, then 817 halted. And if 816 halted via transition C2, then 21, 92, 683 and 818 all halted. A compilation of the various analyses can be found [https://discord.com/channels/960643023006490684/1259770474897080380/1291694606534049793 here]
* {{TM|1RB---0LC_2LC2RC1LB_0RA2RB0LB|undecided}} (21, equivalent to 92 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting]
* {{TM|1RB---1RB_2LC2RC1LB_0RA2RB0LB|undecided}} (92, equivalent to 21 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1213612098232262707 Equivalence claim to 21 by @dyuan1]
* {{TM|1RB2LC---_0LA0RC1LC_1RB2RC1LB|undecided}} (683)
* {{TM|1RB2RA1LB_0LC0RA1LA_---2LA---|undecided}} (816). [https://discord.com/channels/960643023006490684/1259770474897080380/1278398402450817025 See discussion] of likely non-halting by @Rae and @Peacemaker on 28 August 2024
* {{TM|1RB2RA1LB_0LC0RA1LA_---2RB2LA|undecided}} (817)
* {{TM|1RB2RA1LB_0LC0RA1LA_2LA0RB---|undecided}} (818, equivalent to 21 and 92)
[[Category:BB Domain]]

BB(6)

2025-06-25T00:14:36Z

Fr tho: more specific date

The 6-state, 2-symbol Busy Beaver problem, '''BB(6)''', refers to the unsolved 6th value of the [[Busy Beaver function]]. With the discovery of the [[Cryptid]] machine [[Antihydra]] in June 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(6) and thus [https://www.sligocki.com/2024/07/06/bb-6-2-is-hard.html BB(6) is Hard].

The current BB(6) champion {{TM|1RB1LC_1LA1RE_0RD0LA_1RZ1LB_1LD0RF_0RD1RB|halt}} was discovered by mxdys in June 2025, proving the lower bound:

<math display="block">S(6) > \Sigma(6) > 10 \uparrow\uparrow 11010000</math>

== Techniques ==
Simulating tetrational machines, such as the former champion {{TM|1RB0LD_1RC0RF_1LC1LA_0LE1RZ_1LF0RB_0RC0RE|halt}}, requires [[Accelerated simulator|accelerated simulation]] that can handle Collatz Level 2 [[Inductive rule|inductive rules]]. In other words, it requires a simulator that can prove the rules:

<math display="block">\begin{array}{lcl}
C(4k) & \to & {\operatorname{Halt}}\Big(\frac{3^{k+3} - 11}{2}\Big) \\
C(4k+1) & \to & C\Big(\frac{3^{k+3} - 11}{2}\Big) \\
C(4k+2) & \to & C\Big(\frac{3^{k+3} - 11}{2}\Big) \\
C(4k+3) & \to & C\Big(\frac{3^{k+3} + 1}{2}\Big) \\
\end{array}</math>

and also compute the remainder mod 3 of numbers produced by applying these rules 15 times (which requires some fancy math related to [[wikipedia:Euler's_totient_function|Euler's totient function]]).

== Cryptids ==
Several [[Turing machines]] have been found that are [[Cryptids]], considered so because each of them have a [[Collatz-like]] halting problem, a type of problem that is generally difficult to solve. However, probabilistic arguments have allowed all but one of them to be categorized as [[probviously]] halting or probviously non-halting.

Probviously non-halting Cryptids:

* {{TM|1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA}}, [[Antihydra]]
* {{TM|1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA|undecided}}, a variant of [[Hydra]] and Antihydra
* {{TM|1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC|undecided}}, similar to Antihydra
* {{TM|1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---|undecided}}, similar to Antihydra
* {{TM|1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB|undecided}}, similar to Antihydra

Probviously halting Cryptids:

* {{TM|1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA}}, [[Lucy's Moonlight]]
* {{TM|1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC|undecided}}, a family of 16 related TMs
* {{TM|1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF}}
* {{TM|1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB}}
* {{TM|1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA}}
* {{TM|1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE}}
Although {{TM|1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE}} behaves similarly to the probviously halting Cryptids, it is estimated to have a 3/5 chance of becoming a [[translated cycler]] and a 2/5 chance of halting.

There are a few machines considered notable for their chaotic behaviour, but which have not been classified as Cryptids due to seemingly lacking a connection to any known open mathematical problems, such as Collatz-like problems.

Potential Cryptids:

* {{TM|1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE|undecided}}
* {{TM|1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE|undecided}}
* {{TM|1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC|undecided}}
* {{TM|1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD}}

== Top Halters ==
Below is a table of the machines with the 10 highest known runtimes.<ref>Shawn Ligocki's list of 6-state, 2-symbol machines with large runtimes ([https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/6x2.txt Link])</ref> Their sigma scores are expressed using an extension of Knuth's up-arrow notation.<ref>Shawn Ligocki. 2022. [https://www.sligocki.com/2022/06/25/ext-up-notation.html "Extending Up-arrow Notation"]</ref>
{| class="wikitable"
|+Top Known BB(6) Halters
!Standard format
!(approximate) Σ
|-
|{{TM|1RB1LC_1LA1RE_0RD0LA_1RZ1LB_1LD0RF_0RD1RB|halt}}
|10 ↑↑ 11010000
|-
|{{TM|1RB0LD_1RC0RF_1LC1LA_0LE1RZ_1LF0RB_0RC0RE}}
|10 ↑↑ 15.60465
|-
|{{TM|1RB0LF_1RC1RB_1LD0RA_1LB0LE_1RZ0LC_1LA1LF}}
|10 ↑↑ 7.52390
|-
|{{TM|1RB0LF_1RC1RB_1LD0RA_1RF0LE_1RZ0LC_1LA1LF}}
|10 ↑↑ 7.52390
|-
|{{TM|1RB0LF_1RC1RB_1LD0RA_1LF0LE_1RZ0LC_1LA1LF}}
|10 ↑↑ 7.52390
|-
|{{TM|1RB1RC_1LC1RE_1LD0LB_1RE1LC_1LE0RF_1RZ1RA}}
|10 ↑↑ 7.23619
|-
|{{TM|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB}}
|10 ↑↑ 6.96745
|-
|{{TM|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}}
|10 ↑↑ 5.77573
|-
|{{TM|1RB0LA_1LC1LF_0LD0LC_0LE0LB_1RE0RA_1RZ1LD}}
|10 ↑↑ 5.63534
|-
|{{TM|1RB1RE_1LC1LF_1RD0LB_1LE0RC_1RA0LD_1RZ1LC}}
|10 ↑↑ 5.56344
|}
The runtimes are presumed to be about <math>\text{score}^2</math> which is roughly indistinguishable in tetration notation.

== Holdouts ==
@mxdys's informal [[Holdouts lists|holdouts list]] has 3335 machines up to equivalence as of June 2025.

== References ==
<references />
[[Category:BB Domain]]

BB(6)

2025-06-25T00:09:45Z

Fr tho: Updates and formatting

The 6-state, 2-symbol Busy Beaver problem, '''BB(6)''', refers to the unsolved 6th value of the [[Busy Beaver function]]. With the discovery of the [[Cryptid]] machine [[Antihydra]] in 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(6) and thus [https://www.sligocki.com/2024/07/06/bb-6-2-is-hard.html BB(6) is Hard].

The current BB(6) champion {{TM|1RB1LC_1LA1RE_0RD0LA_1RZ1LB_1LD0RF_0RD1RB|halt}} was discovered by mxdys in June 2025, proving the lower bound:

<math display="block">S(6) > \Sigma(6) > 10 \uparrow\uparrow 11010000</math>

== Techniques ==
Simulating tetrational machines, such as the former champion {{TM|1RB0LD_1RC0RF_1LC1LA_0LE1RZ_1LF0RB_0RC0RE|halt}}, requires [[Accelerated simulator|accelerated simulation]] that can handle Collatz Level 2 [[Inductive rule|inductive rules]]. In other words, it requires a simulator that can prove the rules:

<math display="block">\begin{array}{lcl}
C(4k) & \to & {\operatorname{Halt}}\Big(\frac{3^{k+3} - 11}{2}\Big) \\
C(4k+1) & \to & C\Big(\frac{3^{k+3} - 11}{2}\Big) \\
C(4k+2) & \to & C\Big(\frac{3^{k+3} - 11}{2}\Big) \\
C(4k+3) & \to & C\Big(\frac{3^{k+3} + 1}{2}\Big) \\
\end{array}</math>

and also compute the remainder mod 3 of numbers produced by applying these rules 15 times (which requires some fancy math related to [[wikipedia:Euler's_totient_function|Euler's totient function]]).

== Cryptids ==
Several [[Turing machines]] have been found that are [[Cryptids]], considered so because each of them have a [[Collatz-like]] halting problem, a type of problem that is generally difficult to solve. However, probabilistic arguments have allowed all but one of them to be categorized as [[probviously]] halting or probviously non-halting.

Probviously non-halting Cryptids:

* {{TM|1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA}}, [[Antihydra]]
* {{TM|1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA|undecided}}, a variant of [[Hydra]] and Antihydra
* {{TM|1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC|undecided}}, similar to Antihydra
* {{TM|1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---|undecided}}, similar to Antihydra
* {{TM|1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB|undecided}}, similar to Antihydra

Probviously halting Cryptids:

* {{TM|1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA}}, [[Lucy's Moonlight]]
* {{TM|1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC|undecided}}, a family of 16 related TMs
* {{TM|1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF}}
* {{TM|1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB}}
* {{TM|1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA}}
* {{TM|1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE}}
Although {{TM|1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE}} behaves similarly to the probviously halting Cryptids, it is estimated to have a 3/5 chance of becoming a [[translated cycler]] and a 2/5 chance of halting.

There are a few machines considered notable for their chaotic behaviour, but which have not been classified as Cryptids due to seemingly lacking a connection to any known open mathematical problems, such as Collatz-like problems.

Potential Cryptids:

* {{TM|1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE|undecided}}
* {{TM|1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE|undecided}}
* {{TM|1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC|undecided}}
* {{TM|1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD}}

== Top Halters ==
Below is a table of the machines with the 10 highest known runtimes.<ref>Shawn Ligocki's list of 6-state, 2-symbol machines with large runtimes ([https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/6x2.txt Link])</ref> Their sigma scores are expressed using an extension of Knuth's up-arrow notation.<ref>Shawn Ligocki. 2022. [https://www.sligocki.com/2022/06/25/ext-up-notation.html "Extending Up-arrow Notation"]</ref>
{| class="wikitable"
|+Top Known BB(6) Halters
!Standard format
!(approximate) Σ
|-
|{{TM|1RB1LC_1LA1RE_0RD0LA_1RZ1LB_1LD0RF_0RD1RB|halt}}
|10 ↑↑ 11010000
|-
|{{TM|1RB0LD_1RC0RF_1LC1LA_0LE1RZ_1LF0RB_0RC0RE}}
|10 ↑↑ 15.60465
|-
|{{TM|1RB0LF_1RC1RB_1LD0RA_1LB0LE_1RZ0LC_1LA1LF}}
|10 ↑↑ 7.52390
|-
|{{TM|1RB0LF_1RC1RB_1LD0RA_1RF0LE_1RZ0LC_1LA1LF}}
|10 ↑↑ 7.52390
|-
|{{TM|1RB0LF_1RC1RB_1LD0RA_1LF0LE_1RZ0LC_1LA1LF}}
|10 ↑↑ 7.52390
|-
|{{TM|1RB1RC_1LC1RE_1LD0LB_1RE1LC_1LE0RF_1RZ1RA}}
|10 ↑↑ 7.23619
|-
|{{TM|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB}}
|10 ↑↑ 6.96745
|-
|{{TM|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}}
|10 ↑↑ 5.77573
|-
|{{TM|1RB0LA_1LC1LF_0LD0LC_0LE0LB_1RE0RA_1RZ1LD}}
|10 ↑↑ 5.63534
|-
|{{TM|1RB1RE_1LC1LF_1RD0LB_1LE0RC_1RA0LD_1RZ1LC}}
|10 ↑↑ 5.56344
|}
The runtimes are presumed to be about <math>\text{score}^2</math> which is roughly indistinguishable in tetration notation.

== Holdouts ==
@mxdys's informal [[Holdouts lists|holdouts list]] has 3335 machines up to equivalence as of June 2025.

== References ==
<references />
[[Category:BB Domain]]

BB(2,5)

2025-06-24T23:52:33Z

Fr tho: Update holdouts and formatting

The 2-state, 5-symbol Busy Beaver problem, '''BB(2,5)''', is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Hydra]] in April 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(2,5) and thus [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2,5) is Hard].

The current BB(2,5) champion {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}} was discovered by Daniel Yuan in June 2024, proving the lower bounds:

<math display="block">S(2,5) > \Sigma(2,5) > 10^{10^{10^{3\,314\,360}}} > 10 \uparrow\uparrow 4</math>

If it turns out to be the actual champion, it would the only known champion machine that exhibits [[Counter]] behavior.

== Cryptids ==
Known Cryptids:

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA}}, known as [[Hydra]]
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB}}, known as the Bonus Cryptid
Potential Cryptids:

* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}
* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}
* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}
* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}

== Certified progress ==
In April 2024, Shawn Ligocki publicly released a list of 23,411 undecided BB(2,5) machines. Justin Blanchard then made substantial progress over the course of the next month, reducing the list to 499 holdouts by late May 2024. In June 2024, @mxdys cut down the list to 273 using halting and inductive deciders, and again to 217 using [[Closed Tape Language (CTL)|CTL]]. In February 2025, @mxdys ran a decider pipeline in Coq that resulted in only 173 holdouts. Since then, additional machines have been proven in Coq using both deciders and individual proofs.

On [https://discord.com/channels/960643023006490684/1259770421046411285/1355593937531961365 29 Mar 2025], @mxdys published a list of 83 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @mxdys's March 2025 holdouts list of 83 TMs.

=== Cryptids ===

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA|undecided}}. Hydra
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB|undecided}}. Bonus Cryptid

=== Unsolved ===

* {{TM|1RB---4LB1RA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---4LB0LA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}. [https://discord.com/channels/960643023006490684/1354037062830919690/1354037062830919690 Shift overflow counter, potential Cryptid]
* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}. Potential Cryptid
* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}. Potential Cryptid
* {{TM|1RB3LA1LA4LA2RA_2LB2RA---0RA0RB|undecided}}.
* {{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|undecided}}.
* {{TM|1RB---3RA2LA2RB_2LB3LA4LB4RA0RA|undecided}}.
* {{TM|1RB4LA1RA1RB1LA_2LB3LA---4RA2RB|undecided}}. BMO 3 variant?
* {{TM|1RB---4RB2RB4LA_2LB3LA3LB0RA0RB|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353983911222312970 Bouncer + chaotic counter]
* {{TM|1RB2RB3LA4LA1LA_2LB3RA---4RA1RB|undecided}}.
* {{TM|1RB3RB3LA4LA2RB_2LB3RA---1RA1LA|undecided}}.
* {{TM|1RB2LA4LA1RA1LA_2LB3RB4RB---2RA|undecided}}.
* {{TM|1RB4RB4RA1LA3LA_1LB2LA3RB2RB---|undecided}}.
* {{TM|1RB3RA3RB4LA1LA_1LB2LA1LA---1RB|undecided}}. [https://discord.com/channels/960643023006490684/1349602897024782358 Potentially halt]
* {{TM|1RB2RA4LA1RB4RB_1LB2LA3RA---0LB|undecided}}.
* {{TM|1RB3RB1LA2LA3RA_1LB2RA4RB0LA---|undecided}}.
* {{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}.
* {{TM|1RB2LA0RB0LB3LB_2LA4RB3RA0RA---|undecided}}.
* {{TM|1RB2RA3LB---2LB_2LA0LA4RB0RB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329808777754706046 30% chance of beating current champion]
* {{TM|1RB2RA3LB4LA---_2LA0RB1LA2RB0RA|undecided}}. [https://discord.com/channels/960643023006490684/1348878717870673981 Analysis by @dyuan01 and @Legion]
* {{TM|1RB2RA3LA---2LB_2LA4RA4RB0RB0LA|undecided}}. Spaghetti [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 analysis by @nerdyjoe]
* {{TM|1RB2RA3LA4LA2RB_2LA---3LB1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1355112650690003028 Bouncer + chaotic counter]
* {{TM|1RB2RA3LA4LA2RB_2LA3RB---0RA1LA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA1RA4LA2RA_2LA---1LA0RA3RB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA3LB0RB0LA_2LA4RB1LB1RA---|undecided}}.
* {{TM|1RB3LA1LA2RB2RA_2LA4RA3LB1RA---|undecided}}.
* {{TM|1RB3LA3LA0RB2LB_2LA4LA4RA2RA---|undecided}}.
* {{TM|1RB3RA2LB1LB1RB_2LA2RA4LA1LA—--|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RA4LB2RA2RB_2LA---3LA0LB1LA|undecided}}.
* {{TM|1RB2LB3LA0RA1LB_2LA4RA3RB3LA---|undecided}}. [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 Analysis by @nerdyjoe]
* {{TM|1RB2RB---0LB3LA_2LA2LB3RB4RB1LB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB2RB4LA2RA1LA_2LA4RA3LA---3RA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353987502062702622 Longitudinal analysis suggests chaotic]
* {{TM|1RB3LB0RB---2LB_2LA3RA4RB2RB0LA|undecided}}.
* {{TM|1RB3LB4LA0LB---_2LA0LA1RB0RA3RA|undecided}}.
* {{TM|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RB---4RA2RA_2LA2RA3LB4LB1LB|undecided}}.
* {{TM|1RB3RB---0RA2RB_2LA4RA3LB1LB1LA|undecided}}.
* {{TM|1RB3RB1LB2RA---_2LA2RB1LA4LB0RA|undecided}}.
* {{TM|1RB2LA0RB1LA3LB_1LA3LB1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB4LB1RA_1LA3RA1RA---0LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4RB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB3RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LA|undecided}}.
* {{TM|1RB2LA0RB1LB0LB_1LA3RA1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB---4LA_1LA3LA1RA4RA1LB|undecided}}.
* {{TM|1RB2LA0RB4LB0LA_1LA3LA1RA4RA---|undecided}}.
* {{TM|1RB2LA4RA1LA3LA_0LA2RB3RB2LB---|undecided}}. 1D CA-like
* {{TM|1RB2LA4RA1LA3LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA1LA4RA2LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA3LA4RA1LA_0LA3LB3RB1RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA0LB1LA2RA_0LA3RA1RA4LB—--|undecided}}. Potential bouncer
* {{TM|1RB2LA3LB4LB---_0LA4LB3RA4LA0RB|undecided}}. Fractal?

=== Solved with moderate rigor ===

* {{TM|1RB1RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB0RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB4LA1LB2LA0RB_2LB3RB4LA---1RA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 Nonhalting argument by @dyuan]
* {{TM|1RB2RA3LA4LA2RB_2LA---1LA1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA1LA2RA_2LA4RB---0RA0LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA2RB1LA_2LA4RB---3RA3LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB2LB---4LB0RB_1LA3RB4RB4RA1LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Nonhalting argument by @racheline]

=== Formally proven ===

* {{TM|1RB2RA3LA4LA2RB_2LA0RA---0RA1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]
* {{TM|1RB0LB2LA4LB3LA_2LA---3RA4RB2RB|undecided}}. [https://discord.com/channels/960643023006490684/1375251026411786310/1375556785603084469 Coq-decided by @mxdys]
* {{TM|1RB2LA1RA---1LA_1LA4RB3LB0RB2RB|undecided}}. [https://discord.com/channels/960643023006490684/1375251026411786310/1375556785603084469 Coq-decided by @mxdys]
* {{TM|1RB2LA3LA4RA0LA_1LA3RB1RB1LB---|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379521528869421137 Coq-decided by @mxdys]
* {{TM|1RB2RA3LA4RB---_2LA3RB3RA1LB3LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1373347187836194898 Halting argument by @dyuan]
* {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Coq-decided by @mxdys]. Current champion

[[Category:BB Domain]]

BB(4)

2025-05-17T12:38:40Z

Fr tho: Updated introduction for consistency and style fixes

The 4-state, 2-symbol Busy Beaver problem, '''BB(4)''', refers to the 4th value of the [[Busy Beaver function]]. In 1983, the 4-state busy beaver winner was found: a 4-state [[Turing machine]] halting after 107 steps giving the lower bound BB(4) ≥ 107.

In 2024, BB(4) = 107 was officially confirmed by the [[bbchallenge.org]] massively collaborative research project, when a proof for the BB(4) case was added to [[Coq-BB5]] and successfully compiled.<ref>https://github.com/ccz181078/Coq-BB5/blob/main/BB42Theorem.v</ref>

== History ==
In this Section, we use Radó's original S (number of steps) and Σ (number of ones on the final tape) notations; see [[Busy Beaver Functions]].

* In 1965, Allen Brady proves that S(4) ≥ 84 and Σ(4) ≥ 11.<ref name=":0">Brady, A. H. (1965). Solutions of restricted cases of the halting problem applied to the determination of particular values of a non-computable function. https://ir.library.oregonstate.edu/concern/graduate_thesis_or_dissertations/zk51vk21c</ref> (TODO: the abstract says "or ≥ 12 using a different stopping convention")
* In 1966, Allen Brady conjectures Σ(4) = 13 and S(4) = 107 (He says S(4) = 106, but this seems to be based upon a slightly different version of S function).<ref name=":1">Brady, A. H. (1966). The Conjectured Highest Scoring Machines for Rado's Σ(k) for the Value k = 4. https://ieeexplore.ieee.org/document/4038890 </ref>
* In 1974, Allen Brady proves that S(4) = 107.<ref name=":2">https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/</ref> (better source needed)
* In 1983, Allen Brady publishes the proof that Σ(4) = 13 and S(4) = 107. <ref name=":3">Brady, A. H. (1983). The determination of the value of Rado’s noncomputable function Σ(k) for four-state Turing machines. https://www.ams.org/journals/mcom/1983-40-162/S0025-5718-1983-0689479-6/</ref> Some holdouts were not rigorously handled by the proof: ''"All of the remaining holdouts were examined by means of voluminous printouts of their histories along with some program extracted features. It was determined to the author's satisfaction that none of these machines will ever stop."''<ref name=":0" />

== Champions ==
S(4) = 107 and there is only one shift champion (in [[TNF]]):

* {{TM|1RB1LB_1LA0LC_1RZ1LD_1RD0RA|halt}} leaves 13 ones (a ones champion)

Σ(4) = 13 and there are 2 ones champions (in TNF):

* {{TM|1RB1LB_1LA0LC_1RZ1LD_1RD0RA|halt}} runs 107 steps (the steps champion)

* {{TM|1RB0RC_1LA1RA_1RZ1RD_1LD0LB|halt}} runs 96 steps

== Top Halters ==
In [[TNF-1RB]] there are exactly 620,261 BB(4) TMs of which 183,983 halt. The top 20 longest running TMs are:
<pre>
Standard Format Status Steps Σ
1RB1LB_1LA0LC_1RZ1LD_1RD0RA Halt 107 13
1RB1LD_1LC0RB_1RA1LA_1RZ0LC Halt 97 9
1RB0RC_1LA1RA_1RZ1RD_1LD0LB Halt 96 13
1RB1LB_0LC0RD_1RZ1LA_1RA0LA Halt 96 6
1RB1LD_0LC0RC_1LC1LA_1RZ0LA Halt 84 11
1RB1RZ_1LC0RD_1LA1LB_0LC1RD Halt 83 8
1RB0RD_1LC0LA_1RA1LB_1RZ0RC Halt 78 12
1RB1LA_0RC0RD_1LC0LA_1RZ0RC Halt 78 9
1RB0RD_0RC0RA_1LC0LA_0RB1RZ Halt 75 9
1RB0RC_1LC1RA_1RZ0LD_1RA1LA Halt 74 8
1RB1LA_0LA1RC_1RA0RD_1RZ0RB Halt 70 8
1RB1LC_0RC0RB_0LD0LA_1LA1RZ Halt 69 7
1RB1LA_1LA1RC_1RZ0RD_0LD1RB Halt 69 7
1RB1RZ_1LC1RA_0RC0LD_1RD0LB Halt 68 10
1RB0LB_0RC0RD_1LD1LA_0LA1RZ Halt 68 8
1RB1LB_0RC1RZ_1LC1LD_0RD0LA Halt 68 7
1RB0RD_0RC1RZ_1LC0LA_0RA0RB Halt 68 7
1RB0LD_0RC1LD_1LC0RB_0LA1RZ Halt 67 7
1RB1LA_1RC0LD_0LA0RC_1RZ1LB Halt 66 7
1RB1RC_1LC1RD_1RZ0LD_1LA0RA Halt 65 7
</pre>

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

== References ==
<references />
[[Category:BB Domain]]

1RB3LA4RB0RB2LA 1LB2LA3LA1RA1RZ

2025-05-17T12:18:20Z

Fr tho: Transferred information from BB(2,5)

{{machine|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ}}
{{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ}}

This is the current [[BB(2,5)]] champion. It is a halting [[shift overflow counter]] with sigma score (and runtime) over <math>10^{10^{10^{3\,314\,360}}}</math>. It was discovered by Daniel Yuan and shared [https://discord.com/channels/960643023006490684/1084047886494470185/1254826217375273112 on Discord] on 24 Jun 2024 and shared on the busy-beaver-discuss email list [https://groups.google.com/g/busy-beaver-discuss/c/PGOBAz46K6I/m/af5sjd6MBAAJ the next day].

== Analyses ==

=== dyuan01 ===
dyuan01 [https://discord.com/channels/960643023006490684/1084047886494470185/1254826217375273112 24 Jun 2024 11:51am EDT]:<pre>
the TM appears to halt at

[11] [01]^(a+b+c+31) [11]^(d+1) 4 dyuan01 [https://discord.com/channels/960643023006490684/1084047886494470185/1254842225980997793 24 Jun 2024 12:55pm EDT]:<pre>
Alright, so first things first, I should establish some rules, (all variables are natural numbers unless otherwise specified)

Basic rules (all can be simulated in a fixed number of steps):
1) [01] <A -> [11] A>
2) [11] <A -> <A [33]
3) A> [33] -> [01] A>
4) [01] <A3 -> [11] 0B>
5) [11] <A3 -> <A3 [33]
6) 0B> [33] -> [01] 0B>
7) A> [21] -> <A [22]
8) A> [22] -> <A [23]
9) A> [23] -> [41] A>
10) A> 0^inf -> <A [21] 0^inf
11) 0B> [21] -> <A3 [33]
12) 0B> [22] 0^inf -> Halt at [11] 4 [23] -> [11] 0B>
14) [41] <A -> <A [23]
15) 0^inf [11] <A -> 0^inf [11] 0B>

Counter rule helper:
A) [01] [11]^x <A -> [11] [01]^x A> (Basic rules 2*, 1, 3*)

Counter rules:
1) [01] [11]^x <A [23]^y 0^inf -> [11] [01]^x <A [23]^y [21] 0^inf (Counter rule A, Basic rules 9*, 10, 14*)
2) [01] [11]^x <A [23]^y [21] -> [11] [01]^x <A [23]^y [22] (Counter rule A, Basic rules 9*, 7, 14*)
3) [01] [11]^x <A [23]^y [22] -> [11] [01]^x <A [23]^(y+1) (Counter rule A, Basic rules 9*, 8, 14*)
4) 0^inf [11]^(x+1) <A -> 0^inf [11] [01]^x 0B> (Basic rules 2*, 15, 6*)
5) [01] [11]^x <A3 -> [11] [01]^x 0B> (Split <A3 into <A 3, then use Counter rule A, then simulate a step and merge 0 B> into 0B>)

Advanced rules:
1) [01]^3 0B> 0^inf -> [11] [01]^3 <A [21] 0^inf (simulatable in finite steps)
2) [01] [11]^(x+2) 0B> 0^inf -> [11] [01]^x [11]^2 [01] <A [21] 0^inf (Uses Basic rules 2* and 3*, but otherwise can be simulated in finite and bounded steps)

Now, I will simulate some tapes when they are overflowing from certain starting positions (assume 0^inf on both ends and x,y>=2):

(Overflow rule 1)
[11]^x <A [23]^y [21]
[11] [01]^(x-1) 0B> [23]^y [21] (Counter rule 4)
[11] [01]^(x-1) [11]^y 0B> [21] (Basic rule 13*)
[11] [01]^(x-1) [11]^y <A3 [33] (Basic rule 11)
[11] [01]^(x-2) [11] [01]^y 0B> [33] (Counter rule 5)
[11] [01]^(x-2) [11] [01]^(y+1) 0B> (Basic rule 6)
[11] [01]^(x-2) [11] [01]^(y-2) [11] [01]^3 <A [21] (Advanced rule 1)

(Overflow rule 2)
[11]^x <A [23]^y
[11] [01]^(x-1) 0B> [23]^y (Counter rule 4)
[11] [01]^(x-1) [11]^y 0B> (Basic rule 13*)
[11] [01]^(x-2) [11] [01]^(y-2) [11]^2 [01] <A [21] (Advanced rule 2)

(Overflow rule 3)
[11]^x <A [23]^y [22]
[11] [01]^(x-1) 0B> [23]^y [22] (Counter rule 4)
[11] [01]^(x-1) [11]^y 0B> [22] (Basic rule 13*)
Halt at [11] [01]^(x-1) [11]^(y+1) 4 <B 1 (Basic rule 12)

The only steps missing now are the steps to get from (11|01)* <A (21) to (11)* <A (23)* (|21|22), which takes advantage of binary representations and division mod 3.
Now we start to simulate the tape

At some point, the tape reaches [11]^7 <A [23]^17 [21]. By overflow rule 1, we reach
[11] [01]^5 [11] [01]^15 [11] [01]^3 <A [21]

If we treat [11] as 0 and [01] as 1 in binary, then [11] [01]^5 [11] [01]^15 [11] [01]^3 has a binary representation of (2^25-2^19-9). This is divisible by 3, so let a = (2^25-2^19-9)/3 = 11010045 (an odd number). Then we get
[11] [01]^5 [11] [01]^15 [11] [01]^3 <A [21]
[11] [11]^5 [11] [11]^15 [11] [11]^3 <A [23]^a [21]
[11]^26 <A [23]^a [21]

We apply overflow rule 1 again to get
[11] [01]^24 [11] [01]^(a-2) [11] [01]^3 <A [21]

This has a binary representation of 2^(a+27)-2^(a+2)-9, which is 2 mod 3. Let b = (2^(a+27)-2^(a+2)-11)/3, which is an odd number, then we get
[11] [01]^24 [11] [01]^(a-2) [11] [01]^3 <A [21]
[11]^(a+28) <A [23]^(b+1)

Apply overflow rule 2 to get
[11] [01]^(a+26) [11] [01]^(b-1) [11]^2 [01] <A [21]

This has a binary representation of 2^(a+b+29)-2^(b+2)-7, which is also 2 mod 3. Let c = (2^(a+b+29)-2^(b+2)-9)/3, another odd number, then we get
[11]^(a+b+30) <A [23]^(c+1)

We apply overflow rule 2 again to get
[11] [01]^(a+b+28) [11] [01]^(c-1) [11]^2 [01] <A [21]

This has a binary representation of 2^(a+b+c+31)-2^(c+2)-7, which is 1 mod 3. Let d = (2^(a+b+c+31)-2^(c+2)-8)/3. We get
[11]^(a+b+c+32) <A [23]^d [22]

After applying overflow rule 3 we get that this halts at
[11] [01]^(a+b+c+31) [11]^(d+1) 4 Btw, d > 2^c > 2^2^b > 2^2^2^a > 2^2^2^2^23 > 2^2^2^2^2^4 = 2^2^2^2^2^2^2 = 2^^7, so that's probably the lower bound that should be used in steps and sigma for this TM.

LegionMammal978 [https://discord.com/channels/960643023006490684/1084047886494470185/1254967208291991582 24 Jun 2024 9:11pm EDT]:

Assuming your values are correct, HyperCalc and my own manual calculations agree that σ ≈ 2^2^(2.8138364628466968⋅10^3314361) ≈ 10^10^(8.470491782098934⋅10^3314360). Equivalently, this is (2 ↑)⁷ 1.127778888301767 or (10 ↑)⁴ 6.5203998005419574.

=== Shawn Ligocki ===
Shawn Ligocki [https://groups.google.com/g/busy-beaver-discuss/c/PGOBAz46K6I/m/L8hh3KqOBAAJ 25 Jun 2024 1:35am EDT]:

At a high level, this TM satisfies the following rules:

Counter Rules:

* 01 11^x <A 23^y 00 -> 11 01^x <A 23^y 21
* 01 11^x <A 23^y 21 -> 11 01^x <A 23^y 22
* 01 11^x <A 23^y 22 -> 11 01^x <A 23^y 23

In other words, each iteration, the left counts up 1 in a binary counter (using "01" for 0 and "11" for 1) while the right keeps track of the number of iterations modulo 3 (using the final value of "21", "22" or "23") and grows every 3 iterations.

This continues until the counter "overflows" and depending upon the mod on the right side it has one of 3 possible behaviors.

Overflow Rules:

* 0^inf 11^x+2 <A 23^y+2 0^inf -> 0^inf 11 01^x 11 01^y 11^2 01 <A 21 0^inf
* 0^inf 11^x+2 <A 23^y+2 21 0^inf -> 0^inf 11 01^x 11 01^y 11 01^3 <A 21 0^inf
* 0^inf 11^x+1 <A 23^y+1 22 0^inf -> 0^inf 11 01^x 11^y+2 1 Z> 1 0^inf

I have [https://github.com/sligocki/busy-beaver/commit/3189833014f1b2442d4ffe91c6e1d7fdb574675a confirmed] all of the above rules in my inductive validator.

At step 2430 it is in config "0^inf 11^7 <A 23^17 21 0^inf" and Daniel reports that it proceeds to overflow 5 times with the last one hitting the halt rule (I have not confirmed this behavior yet myself). The penultimate config reported by Daniel is:<pre>
0^inf [11] [01]^(a+b+c+31) [11]^(d+1) 4 Where<pre>
a = (2^25-2^19-9)/3 = 11010045
b = [2^(a+27)-2^(a+2)-11]/3
c = [2^(a+b+29)-2^(b+2)-9]/3
d = [2^(a+b+c+31)-2^(c+2)-8]/3
</pre>and Mathew House on Discord reported that this makes the sigma value for this TM > (10 ↑)^4 6.5

=== Pascal Michel ===
Pascal Michel [https://groups.google.com/g/busy-beaver-discuss/c/PGOBAz46K6I/m/ptLo9T7NCQAJ 15 Jan 2025 2:58am EST]:

Let M be the 2x5 TM found by Daniel Yuan in June 2024, with s(M) > 10^(10^(10^3314360)).

Here, I give a proof that s(M) is approximately 3/2 (sigma(M)^2).

(1) Time for

- Counter rules:

01 (11)^x <A (23)^y 00 --( 4(x + y) + 6 )--> 11 (01)^x <A (23)^y 21

01 (11)^x <A (23)^y 21 --( 4(x + y) + 6 )--> 11 (01)^x <A (23)^y 22

01 (11)^x <A (23)^y 22 --( 4(x + y) = 6 )--> 11 (01)^x <A (23)^y 23

so we have

. . . <A (23)^y 00 --( . . . + 12y + . . . )--> . . . <A (23)^(y + 1)

- Overflow rules:

0 (11)^(x + 2) <A (23)^(y + 2) 0^3 --( 4x + 8y + 53 )--> 11 (01)^x 11 (01)^y 01 <A 21

0 (11)^(x + 2) <A (23)^(y + 2) 21 0^3 --( 4x + 8y + 73 )--> 11 (01)^x 11 (01)^y 11 (01)^3 <A 21

0 (11)^(x + 1) <A (23)^(y + 1) 22 0 --( 4(x + y) + 15 )--> 11 (01)^x (11)^(y + 2) 1 Z>1

(2) The time taken on the binary counter is linear in the number of binary steps, so it is dominated by the time taken on the 23s, which is quadratic.

(3) The total time is dominated by the time taken from the 4th overflow to the last overflow.

Just before the last overflow, the configuration is

. . . <A (23)^d 22 0^inf

So the total time is

T ~= (12x1) + (12x2) + . . . +(12x(d - 1)) = 12(d - 1)d/2 ~= 6 d^2

We have sigma(M) ~= 2d, so s(M) ~= 3/2 (sigma(M)^2).

=== racheline ===
racheline [https://discord.com/channels/960643023006490684/1084047886494470185/1329499932847243424 16 Jan 2025 12:18 PM EST]:<pre>
for i in {1,2,3}, (3(a+2)+i,b) is <A 3^(2b+2) (23)^a 2 i
(3k+1,n) -> ((2^n-1)*2^k-2,n+k)
(3k+2,n) -> halt
(3k+3,n) -> ((2^n-1)*2^k,n+k)
start from (58,6)

(58,6) -> (3a+1,25) -> (3b+3,a+25) -> (3c+3,a+b+25) -> (3d+2,a+b+c+25) -> halt
where
a = 11010047
b = ((2^25-1)*2^a-5)/3
c = ((2^(a+25)-1)*2^b-3)/3
d = ((2^(a+b+25)-1)*2^c-2)/3
it halts with exactly a+b+c+25+2d+2 = a+b+c+2d+27 ones on the tape (and no other nonzero symbols)
</pre>

BB(2,5)

2025-05-17T12:16:58Z

Fr tho: Updated introduction for consistency and style fixes

The 2-state, 5-symbol Busy Beaver problem, '''BB(2,5)''', is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Hydra]] in April 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(2,5) and thus [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2,5) is Hard].

The current BB(2,5) champion {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}} was discovered by Daniel Yuan in June 2024, proving the lower bounds:

<math display="block">S(2,5) > \Sigma(2,5) > 10^{10^{10^{3\,314\,360}}} > 10 \uparrow\uparrow 4</math>

If it turns out to be the actual champion, it would the only known champion machine that exhibits [[Counter]] behavior.

== Cryptids ==
Known BB(2,5) Cryptids

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA}}, known as [[Hydra]].
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB}}, known as the bonus cryptid

== Certified progress ==
In April 2024, Shawn Ligocki publicly released a list of 23,411 undecided BB(2,5) machines. Justin Blanchard then made substantial progress over the course of the next month, reducing the list to 499 holdouts by late May 2024. In June 2024, @mxdys cut down the list to 273 using halting and inductive deciders, and again to 217 using [[Closed Tape Language (CTL)|CTL]]. In February 2025, @mxdys ran a decider pipeline in Coq that resulted in only 173 holdouts. Since then, additional machines have been proven in Coq using both deciders and individual proofs.

On [https://discord.com/channels/960643023006490684/1259770421046411285/1355593937531961365 29 Mar 2025], @mxdys published a list of 83 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @mxdys's March 2025 holdouts list of 83 TMs.

=== Cryptids ===

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA|undecided}}. Hydra
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB|undecided}}. Bonus cryptid

=== Unsolved ===

* {{TM|1RB---4LB1RA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---4LB0LA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}. [https://discord.com/channels/960643023006490684/1354037062830919690/1354037062830919690 Shift overflow counter, potential cryptid]
* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}. Potential cryptid
* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}. Potential cryptid
* {{TM|1RB3LA1LA4LA2RA_2LB2RA---0RA0RB|undecided}}.
* {{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|undecided}}.
* {{TM|1RB---3RA2LA2RB_2LB3LA4LB4RA0RA|undecided}}.
* {{TM|1RB4LA1RA1RB1LA_2LB3LA---4RA2RB|undecided}}. BMO 3 variant?
* {{TM|1RB---4RB2RB4LA_2LB3LA3LB0RA0RB|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353983911222312970 Bouncer + chaotic counter]
* {{TM|1RB2RB3LA4LA1LA_2LB3RA---4RA1RB|undecided}}.
* {{TM|1RB3RB3LA4LA2RB_2LB3RA---1RA1LA|undecided}}.
* {{TM|1RB2LA4LA1RA1LA_2LB3RB4RB---2RA|undecided}}.
* {{TM|1RB4RB4RA1LA3LA_1LB2LA3RB2RB---|undecided}}.
* {{TM|1RB3RA3RB4LA1LA_1LB2LA1LA---1RB|undecided}}. [https://discord.com/channels/960643023006490684/1349602897024782358 Potentially halt]
* {{TM|1RB2RA4LA1RB4RB_1LB2LA3RA---0LB|undecided}}.
* {{TM|1RB3RB1LA2LA3RA_1LB2RA4RB0LA---|undecided}}.
* {{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}.
* {{TM|1RB2LA0RB0LB3LB_2LA4RB3RA0RA---|undecided}}.
* {{TM|1RB2RA3LB---2LB_2LA0LA4RB0RB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329808777754706046 30% chance of beating current champion]
* {{TM|1RB2RA3LB4LA---_2LA0RB1LA2RB0RA|undecided}}. [https://discord.com/channels/960643023006490684/1348878717870673981 Analysis by @dyuan01 and @Legion]
* {{TM|1RB2RA3LA---2LB_2LA4RA4RB0RB0LA|undecided}}. Spaghetti [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 analysis by @nerdyjoe]
* {{TM|1RB2RA3LA4LA2RB_2LA---3LB1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1355112650690003028 Bouncer + chaotic counter]
* {{TM|1RB2RA3LA4LA2RB_2LA3RB---0RA1LA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA1RA4LA2RA_2LA---1LA0RA3RB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA3LB0RB0LA_2LA4RB1LB1RA---|undecided}}.
* {{TM|1RB3LA1LA2RB2RA_2LA4RA3LB1RA---|undecided}}.
* {{TM|1RB3LA3LA0RB2LB_2LA4LA4RA2RA---|undecided}}.
* {{TM|1RB3RA2LB1LB1RB_2LA2RA4LA1LA—--|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RA4LB2RA2RB_2LA---3LA0LB1LA|undecided}}.
* {{TM|1RB0LB2LA4LB3LA_2LA---3RA4RB2RB|undecided}}.
* {{TM|1RB2LB3LA0RA1LB_2LA4RA3RB3LA---|undecided}}. [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 Analysis by @nerdyjoe]
* {{TM|1RB2RB---0LB3LA_2LA2LB3RB4RB1LB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB2RB4LA2RA1LA_2LA4RA3LA---3RA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353987502062702622 Longitudinal analysis suggests chaotic]
* {{TM|1RB3LB0RB---2LB_2LA3RA4RB2RB0LA|undecided}}.
* {{TM|1RB3LB4LA0LB---_2LA0LA1RB0RA3RA|undecided}}.
* {{TM|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RB---4RA2RA_2LA2RA3LB4LB1LB|undecided}}.
* {{TM|1RB3RB---0RA2RB_2LA4RA3LB1LB1LA|undecided}}.
* {{TM|1RB3RB1LB2RA---_2LA2RB1LA4LB0RA|undecided}}.
* {{TM|1RB2LA1RA---1LA_1LA4RB3LB0RB2RB|undecided}}. Fractal?
* {{TM|1RB2LA3LA4RA0LA_1LA3RB1RB1LB---|undecided}}. Fractal?
* {{TM|1RB2LA0RB1LA3LB_1LA3LB1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB4LB1RA_1LA3RA1RA---0LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4RB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB3RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LA|undecided}}.
* {{TM|1RB2LA0RB1LB0LB_1LA3RA1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB---4LA_1LA3LA1RA4RA1LB|undecided}}.
* {{TM|1RB2LA0RB4LB0LA_1LA3LA1RA4RA---|undecided}}.
* {{TM|1RB2LA4RA1LA3LA_0LA2RB3RB2LB---|undecided}}. 1D CA-like
* {{TM|1RB2LA4RA1LA3LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA1LA4RA2LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA3LA4RA1LA_0LA3LB3RB1RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA0LB1LA2RA_0LA3RA1RA4LB—--|undecided}}. Potential bouncer
* {{TM|1RB2LA3LB4LB---_0LA4LB3RA4LA0RB|undecided}}. Fractal?

=== Solved with moderate rigor ===

* {{TM|1RB1RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB0RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB4LA1LB2LA0RB_2LB3RB4LA---1RA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 Nonhalting argument by @dyuan]
* {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---|undecided}}. Current champion
* {{TM|1RB2RA3LA4RB---_2LA3RB3RA1LB3LB|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1256293368909004820 Counter] that halts in at most 56452325275 steps
* {{TM|1RB2RA3LA4LA2RB_2LA---1LA1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA1LA2RA_2LA4RB---0RA0LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA2RB1LA_2LA4RB---3RA3LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB2LB---4LB0RB_1LA3RB4RB4RA1LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Nonhalting argument by @racheline]

=== Formally proven ===

* {{TM|1RB2RA3LA4LA2RB_2LA0RA---0RA1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]

[[Category:BB Domain]]

BB(3,3)

2025-05-17T12:04:47Z

Fr tho: Style

The 3-state, 3-symbol Busy Beaver problem, '''BB(3,3)''', is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Bigfoot]] in 2023, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(3,3) and thus [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3,3) is Hard].

The current BB(3,3) champion {{TM|0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC|halt}} was discovered by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in 2007, proving the lower bounds:

<math display="block">\begin{array}{lcrl}
S(3, 3) & \ge & 119{,}112{,}334{,}170{,}342{,}541 & > 10^{17} \\
\Sigma(3, 3) & \ge & 374{,}676{,}383 & > 10^8 \\
\end{array}</math>

One of the 6 currently unsolved TMs, {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}, is under very active exploration in channel #bb3x3 and believed to be a [[probviously]] halting TM by some members. If it halts, it will be the new champion.

== Cryptids ==
Known BB(3,3) Cryptids:
* {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}, known as [[Bigfoot]]
Possibly probviously halting Cryptid:

* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}

== Top Halters ==
The current top 10 BB(3,3) halters (known by [[User:sligocki|Shawn Ligocki]]) are:
<pre>
Standard format Status S Σ
0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC Halt 119112334170342541 374676383
1RB2LA1LC_0LA2RB1LB_1RZ1RA1RC Halt 119112334170342540 374676383
1RB2RC1LA_2LA1RB1RZ_2RB2RA1LC Halt 4345166620336565 95524079
1RB1LA2LC_2LA2RB1RB_1RZ0LB0RC Halt 452196003014837 21264944
1RB1RZ2LC_1LC2RB1LB_1LA2RC2LA Halt 4144465135614 2950149
1RB2LA1RA_1RC2RB0RC_1LA1RZ1LA Halt 987522842126 1525688
1RB1RZ2RB_1LC0LB1RA_1RA2LC1RC Halt 4939345068 107900
1RB2LA1RA_1LB1LA2RC_1RZ1LC2RB Halt 1808669066 43925
1RB2LA1RA_1LC1LA2RC_1RZ1LA2RB Halt 1808669046 43925
1RB2LA1RA_1LB1LA2RC_1RZ1LA2RB Halt 1808669046 43925
</pre>
Numbers listed are step count and sigma score for each TM. For a longer list of halting TMs see https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/3x3. For historical perspective see Pascal Michel's [https://bbchallenge.org/~pascal.michel/ha#tm33 '''Historical survey of Busy Beavers'''].

== Certified Progress ==
On [https://discord.com/channels/960643023006490684/1259770474897080380/1325592156257124443 5 Jan 2025], @tjligocki finished an enumeration and filtering of the BB(3,3) machines using the established Ligocki filters, listing the filter used for each machine. He also computed the number of steps and sigma scores for all found halting TMs. The thorough results are located [https://drive.google.com/drive/folders/101U9htddFdE889agAZnU58VLgQJlfn0v?usp=drive_link here]. 367 machines remained on that list. These results were updated on [https://discord.com/channels/960643023006490684/1259770474897080380/1352398469456859167 20 Mar 2025] in the same location and 76 machines remained on the list.

Over two-thirds of the 367 remaining machines were shown to be non-halting with FAR and MITMWFAR by @Justin Blanchard on [https://discord.com/channels/960643023006490684/1259770474897080380/1262265485639286876 14 July 2024]. Most of the remainders were shown non-halting by @lijil on [https://discord.com/channels/960643023006490684/1084047886494470185/1116351783040716830 8 June 2023.] Together, this leaves 21 unsolved TMs, all of which were on @Justin Blanchard's informal holdouts list of 22 machines (see below). The extra machine on Justin's list {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} had been solved by @lijil before, but this was not realized for some time.

On [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 26 Feb 2025], @mxdys published a list of 19 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @Justin Blanchard's June 2024 informal [[Holdouts lists|holdouts list]] of 22 TMs.

=== Cryptids ===
* 829: Bigfoot: {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}

=== Unsolved ===
* {{TM|1RB1LB2LC_1LA2RB1RB_---0LA2LA|undecided}} (397)
* {{TM|1RB0LB0RC_2LC2LA1RA_1RA1LC---|undecided}} (153, equivalent to 758)
* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}} (758, equivalent to 153)
* Wily Coyote: {{TM|1RB2LA1LA_2LA0RA2RC_---0LC2RA|undecided}} (531, equivalent to 532)
* {{TM|1RB2LA1LA_2LA0RA2RC_---1RB2RA|undecided}} (532, equivalent to 531)

=== Solved with moderate rigor ===
* {{TM|1RB2LA1LC_1LA2RB1RB_---2LB0LC|undecided}} (543). See argument for non-halting by @dyuan on [https://discord.com/channels/960643023006490684/1084047886494470185/1240854539519791216 16 May 2024] and [https://discord.com/channels/960643023006490684/1259770474897080380/1325646208483590177 5 January 2025]
* {{TM|1RB1LC1LC_1LA2RB0RB_2LB---0LA|undecided}} (412) ([https://cosearch.bbchallenge.org/contribution/f9gdw0mg cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1279055891559223399 Longitudinal analysis by @Legion implies non-halting]
* {{TM|1RB2LB0LC_2LA2RA1RB_---2LA1LC|undecided}} (650) ([https://cosearch.bbchallenge.org/contribution/32099ui7 cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1290044219481657476 Longitudinal analysis (with extra typo disclaimer) by @Legion implies non-halting]

* {{TM|1RB0RC---_2RC0LB1LB_2LC2RA2RB|undecided}} (279). [https://discord.com/channels/960643023006490684/1084047886494470185/1256729514076016733 Longitudinal analysis by @Legion implies non-halting]
* {{TM|1RB2RB1LC_1LA2RB0RB_2LB---0LA|undecided}} (867). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting]

=== Formally proven ===
* {{TM|1RB1LC---_0LC2RB1LB_2LA0RC1RC|undecided}} (400, equivalent to 494). [https://discord.com/channels/960643023006490684/1218877181321678928/1265131102289264690 Coq proof by @-d]. [https://discord.com/channels/960643023006490684/1084047886494470185/1215532512307052634 Equivalence argument provided by @Legion]

* {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} (494, equivalent to 400, non-halting certified on @lijil's list, equivalence not certified)
* {{TM|1RB2LA2RA_1LC1LB0RA_2RA0LB---|undecided}} (637) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys]. Analyzed by [https://discord.com/channels/960643023006490684/1084047886494470185/1211655096098885732 @Justin], proven by [https://discord.com/channels/960643023006490684/1084047886494470185/1222028527755460700 @dyuan] and [https://discord.com/channels/960643023006490684/1259770474897080380/1327101773604720730 @Andrew]
* {{TM|1RB2LB---_1RC2RB1LC_0LA0RB1LB|undecided}} (642, related to Group 1) ([https://cosearch.bbchallenge.org/contribution/3wxkcx6f cosearch]). Coq proof by @-d. [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan
* {{TM|1RB2RB---_1LC2LB1RC_0RA0LB1RB|undecided}} (834) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys] [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan, who noted a similarity to 642
The following TMs were Coq-decided individually [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 by @mxdys], but analysis beforehand showed their halting problems were highly dependent on that of machine 816. If it was non-halting, then 21, 92, 683, 817, and 818 were all non-halting. If 816 halted via transition C0, then 817 halted. And if 816 halted via transition C2, then 21, 92, 683 and 818 all halted. A compilation of the various analyses can be found [https://discord.com/channels/960643023006490684/1259770474897080380/1291694606534049793 here]
* {{TM|1RB---0LC_2LC2RC1LB_0RA2RB0LB|undecided}} (21, equivalent to 92 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting]
* {{TM|1RB---1RB_2LC2RC1LB_0RA2RB0LB|undecided}} (92, equivalent to 21 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1213612098232262707 Equivalence claim to 21 by @dyuan1]
* {{TM|1RB2LC---_0LA0RC1LC_1RB2RC1LB|undecided}} (683)
* {{TM|1RB2RA1LB_0LC0RA1LA_---2LA---|undecided}} (816). [https://discord.com/channels/960643023006490684/1259770474897080380/1278398402450817025 See discussion] of likely non-halting by @Rae and @Peacemaker on 28 August 2024
* {{TM|1RB2RA1LB_0LC0RA1LA_---2RB2LA|undecided}} (817)
* {{TM|1RB2RA1LB_0LC0RA1LA_2LA0RB---|undecided}} (818, equivalent to 21 and 92)
[[Category:BB Domain]]

BB(2,4)

2025-05-17T11:56:04Z

Fr tho: better description

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 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.<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>
* [[User:tjligocki|Terry]] and [[User:sligocki|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]]):
* {{TM|1RB2LA1RA1RA_1LB1LA3RB1RZ|halt}}

== Top Halters ==
The top 20 longest running BB(2,4) TMs (in [[TNF-1RB]]) are:
<pre>
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
</pre>

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 Domain]]

BB(5)

2025-05-17T11:52:51Z

Fr tho: Updated introduction for consistency

The 5-state, 2-symbol Busy Beaver problem, '''BB(5)''', refers to the 5th value of the [[Busy Beaver function]]. In 1989, the [[5-state busy beaver winner]] was found: a 5-state [[Turing machine]] halting after 47,176,870 steps giving the lower bound BB(5) ≥ 47,176,870.<ref name=":0">H. Marxen and J. Buntrock. Attacking the Busy Beaver 5. Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html</ref>

In 2024, BB(5) = 47,176,870 was proven by the [[bbchallenge.org]] massively collaborative research project.

== History ==
In this Section, we use Radó's original S (number of steps) and Σ (number of ones on the final tape) notations, see [[Busy Beaver Functions]].

=== Finding the 5-state winner ===

* In 1964, Green establishes Σ(5) ≥ 17.<ref name=":1">Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52 </ref>
* In 1972, Lynn establishes S(5) ≥ 435 and Σ(5) ≥ 22.<ref name=":1" />
* In 1973, Weimann establishes S(5) ≥ 556 and Σ(5) ≥ 40.<ref name=":1" />
* In 1974, Lynn, cited by Brady (1983)<ref>Brady, A.H. (1983). The determination of the value of Rado’s noncomputable function Σ() for four-state Turing machines. ''Mathematics of Computation, 40'', 647-665.</ref>, establishes S(5) ≥ 7,707 and Σ(5) ≥ 112.
* In 1983, the [https://docs.bbchallenge.org/other/lud20.pdf Dortmund contest]is organised to find new 5-state champions, winner is Uwe Schult who established S(5) ≥ 134,467 and Σ(5) ≥ 501.
* In 1984, George Uhing establishes S(5) ≥ 2,133,492 and Σ(5) ≥ 1,915.<ref>https://docs.bbchallenge.org/other/busy.html</ref>
* In 1989, Heiner and Buntrock find the [[5-state busy beaver winner]], establishing S(5) ≥ 47,176,870 and Σ(5) ≥ 4,098.<ref name=":0" /> They do not prove (or claim) that the machine is the actual winner (i.e. that no other 5-state machines halt after more steps) but they present some ideas for automatically deciding the behavior of Turing machines (i.e. making [[Deciders]]).<ref name=":0" />

=== Proving that the 5-state winner is actually the winner ===
No machine halting in more steps than the [[5-state busy beaver winner]] has been found since 1989, hinting that it is actually the 5-state winner (i.e. no 5-state machine could halt after more steps). In 2020, Scott Aaronson formally conjectured that BB(5) = 47,176,870.<ref>Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. <nowiki>https://doi.org/10.1145/3427361.3427369</nowiki></ref> In practice, proving this conjecture requires to study the behavior of ~100 million 5-state machines.<ref>https://bbchallenge.org/method</ref>
* In 2003, Georgi Georgiev (Skelet) publishes a list of [[Skelet's 43 holdouts|43 holdouts]], based on [[bbfind]], a collection of [[Deciders]] written in Pascal.<ref>https://skelet.ludost.net/bb/index.html</ref>
* In 2009, Joachim Hertel publishes a method claiming 100 holdouts.<ref>Function, S., & Hertel, J. (2009). Computing the Uncomputable Rado Sigma Function. https://www.mathematica-journal.com/2009/11/23/computing-the-uncomputable-rado-sigma-function/</ref>
* In 2022, [[bbchallenge.org]] is released, with the aim of collaboratively proving that BB(5) = 47,176,870.<ref>https://bbchallenge.org/story</ref>
* In 2024, bbchallenge's contributor @mxdys publishes [[Coq-BB5]], a Coq-verified proof of BB(5) = 47,176,870<ref>https://github.com/ccz181078/Coq-BB5</ref>, ending a 60 years old quest. This proof uses and/or improves on many other bbchallenge's contributions, see [[Coq-BB5]].

== Champions ==
S(5) = 47,176,870 and there is only one shift champion (in [[TNF]]):

* {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} leaves 4098 ones (a ones champion)

Σ(5) = 4098 and there are 2 ones champions (in TNF):

* {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} runs for 47,176,870 steps (the steps champion)
* {{TM|1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC|halt}} runs for 11,798,826 steps

== Top Halters ==
The top 20 longest running BB(5) TMs (in [[TNF-1RB]]) are:
<pre>
Standard format Status S Σ
1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA Halt 47176870 4098
1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt 23554764 4097
1RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ0RB Halt 11821234 4097
1RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ0RB Halt 11821220 4097
1RB1RA_0LC0RC_1RZ1RD_1LE0LA_1LA1LE Halt 11821190 4096
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC0LA Halt 11815076 4096
1RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ1LC Halt 11811040 4097
1RB1RA_1LC1LB_0RC1LD_1RA0LE_1RZ1LC Halt 11811040 4097
1RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ1LC Halt 11811026 4097
1RB1RA_0LC0RC_1RZ1RD_1LE1RB_1LA1LE Halt 11811010 4096
1RB1RA_1LC1LB_1RA1LD_0RE0LE_1RZ1LC Halt 11804940 4097
1RB1RA_1LC1LB_1RA1LD_1RA0LE_1RZ1LC Halt 11804926 4097
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_0LE1RB Halt 11804910 4096
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC1RB Halt 11804896 4096
1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC Halt 11798826 4098
1RB1RA_1LC1RD_1LA1LC_1RZ0RE_1LC1RB Halt 11798796 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_0LE0RB Halt 11792724 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_1LA0RB Halt 11792696 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt 11792682 4097
1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA Halt 2358064 1471
</pre>
For more top halting BB(5) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/5x2

== References ==
<references />
[[Category:BB Domain]]

BB(2,4)

2025-05-17T11:52:38Z

Fr tho: Improved introduction

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 2005.

On August 22, 2024, BB(2,4) = 3,932,964 was officially confirmed by the bbchallenge 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.<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>
* [[User:tjligocki|Terry]] and [[User:sligocki|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]]):
* {{TM|1RB2LA1RA1RA_1LB1LA3RB1RZ|halt}}

== Top Halters ==
The top 20 longest running BB(2,4) TMs (in [[TNF-1RB]]) are:
<pre>
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
</pre>

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 Domain]]

BB(2,4)

2025-05-17T11:41:32Z

Fr tho: Update halters section and introduction for consistency

The 2-state, 4-symbol Busy Beaver problem, '''BB(2,4)''', was officially found to be 3,932,964 on August 22, 2024 by the bbchallenge project, when a proof for the BB(2,4) case was added to [[Coq-BB5]] and successfully compiled. The champion machine M, has S(M) = 3,932,964 and Σ(M) = 2,050.

== 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>
* [[User:tjligocki|Terry]] and [[User:sligocki|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]]):
* {{TM|1RB2LA1RA1RA_1LB1LA3RB1RZ|halt}}

== Top Halters ==
The top 20 longest running BB(2,4) TMs (in [[TNF-1RB]]) are:
<pre>
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
</pre>

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 Domain]]

BB(5)

2025-05-17T11:30:13Z

Fr tho: Update halters section for consistency

The 5-state 2-symbol Busy Beaver problem, '''BB(5)''', refers to the 5th value of the [[Busy Beaver function]]. In 1989, the [[5-state busy beaver winner]] was found: a 5-state [[Turing machine]] halting after 47,176,870 giving the lower bound BB(5) ≥ 47,176,870.<ref name=":0">H. Marxen and J. Buntrock. Attacking the Busy Beaver 5. Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html</ref>

In 2024, BB(5) = 47,176,870 was proven by the [[bbchallenge.org]] massively collaborative research project.

== History ==
In this Section, we use Radó's original S (number of steps) and Σ (number of ones on the final tape) notations, see [[Busy Beaver Functions]].

=== Finding the 5-state winner ===

* In 1964, Green establishes Σ(5) ≥ 17.<ref name=":1">Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52 </ref>
* In 1972, Lynn establishes S(5) ≥ 435 and Σ(5) ≥ 22.<ref name=":1" />
* In 1973, Weimann establishes S(5) ≥ 556 and Σ(5) ≥ 40.<ref name=":1" />
* In 1974, Lynn, cited by Brady (1983)<ref>Brady, A.H. (1983). The determination of the value of Rado’s noncomputable function Σ() for four-state Turing machines. ''Mathematics of Computation, 40'', 647-665.</ref>, establishes S(5) ≥ 7,707 and Σ(5) ≥ 112.
* In 1983, the [https://docs.bbchallenge.org/other/lud20.pdf Dortmund contest]is organised to find new 5-state champions, winner is Uwe Schult who established S(5) ≥ 134,467 and Σ(5) ≥ 501.
* In 1984, George Uhing establishes S(5) ≥ 2,133,492 and Σ(5) ≥ 1,915.<ref>https://docs.bbchallenge.org/other/busy.html</ref>
* In 1989, Heiner and Buntrock find the [[5-state busy beaver winner]], establishing S(5) ≥ 47,176,870 and Σ(5) ≥ 4,098.<ref name=":0" /> They do not prove (or claim) that the machine is the actual winner (i.e. that no other 5-state machines halt after more steps) but they present some ideas for automatically deciding the behavior of Turing machines (i.e. making [[Deciders]]).<ref name=":0" />

=== Proving that the 5-state winner is actually the winner ===
No machine halting in more steps than the [[5-state busy beaver winner]] has been found since 1989, hinting that it is actually the 5-state winner (i.e. no 5-state machine could halt after more steps). In 2020, Scott Aaronson formally conjectured that BB(5) = 47,176,870.<ref>Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. <nowiki>https://doi.org/10.1145/3427361.3427369</nowiki></ref> In practice, proving this conjecture requires to study the behavior of ~100 million 5-state machines.<ref>https://bbchallenge.org/method</ref>
* In 2003, Georgi Georgiev (Skelet) publishes a list of [[Skelet's 43 holdouts|43 holdouts]], based on [[bbfind]], a collection of [[Deciders]] written in Pascal.<ref>https://skelet.ludost.net/bb/index.html</ref>
* In 2009, Joachim Hertel publishes a method claiming 100 holdouts.<ref>Function, S., & Hertel, J. (2009). Computing the Uncomputable Rado Sigma Function. https://www.mathematica-journal.com/2009/11/23/computing-the-uncomputable-rado-sigma-function/</ref>
* In 2022, [[bbchallenge.org]] is released, with the aim of collaboratively proving that BB(5) = 47,176,870.<ref>https://bbchallenge.org/story</ref>
* In 2024, bbchallenge's contributor @mxdys publishes [[Coq-BB5]], a Coq-verified proof of BB(5) = 47,176,870<ref>https://github.com/ccz181078/Coq-BB5</ref>, ending a 60 years old quest. This proof uses and/or improves on many other bbchallenge's contributions, see [[Coq-BB5]].

== Champions ==
S(5) = 47,176,870 and there is only one shift champion (in [[TNF]]):

* {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} leaves 4098 ones (a ones champion)

Σ(5) = 4098 and there are 2 ones champions (in TNF):

* {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} runs for 47,176,870 steps (the steps champion)
* {{TM|1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC|halt}} runs for 11,798,826 steps

== Top Halters ==
The top 20 longest running BB(5) TMs (in [[TNF-1RB]]) are:
<pre>
Standard format Status S Σ
1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA Halt 47176870 4098
1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt 23554764 4097
1RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ0RB Halt 11821234 4097
1RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ0RB Halt 11821220 4097
1RB1RA_0LC0RC_1RZ1RD_1LE0LA_1LA1LE Halt 11821190 4096
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC0LA Halt 11815076 4096
1RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ1LC Halt 11811040 4097
1RB1RA_1LC1LB_0RC1LD_1RA0LE_1RZ1LC Halt 11811040 4097
1RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ1LC Halt 11811026 4097
1RB1RA_0LC0RC_1RZ1RD_1LE1RB_1LA1LE Halt 11811010 4096
1RB1RA_1LC1LB_1RA1LD_0RE0LE_1RZ1LC Halt 11804940 4097
1RB1RA_1LC1LB_1RA1LD_1RA0LE_1RZ1LC Halt 11804926 4097
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_0LE1RB Halt 11804910 4096
1RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC1RB Halt 11804896 4096
1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC Halt 11798826 4098
1RB1RA_1LC1RD_1LA1LC_1RZ0RE_1LC1RB Halt 11798796 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_0LE0RB Halt 11792724 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_1LA0RB Halt 11792696 4097
1RB1RA_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt 11792682 4097
1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA Halt 2358064 1471
</pre>
For more top halting BB(5) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/5x2

== References ==
<references />
[[Category:BB Domain]]

BB(3,3)

2025-05-17T11:29:26Z

Fr tho: Update halters list format for consistency

The 3-state, 3-symbol Busy Beaver problem '''BB(3,3)''' is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Bigfoot]] in 2023, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(3,3) and thus [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3,3) is Hard].

The current BB(3,3) champion {{TM|0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC|halt}} was discovered by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in 2007, proving the lower bounds:

<math display="block">\begin{array}{lcrl}
S(3, 3) & \ge & 119{,}112{,}334{,}170{,}342{,}541 & > 10^{17} \\
\Sigma(3, 3) & \ge & 374{,}676{,}383 & > 10^8 \\
\end{array}</math>

One of the 6 currently unsolved TMs, {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}, is under very active exploration in channel #bb3x3 and believed to be a [[probviously]] halting TM by some members. If it halts, it will be the new champion.

== Cryptids ==
Known BB(3,3) Cryptids:
* {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}, known as [[Bigfoot]]
Possibly probviously halting Cryptid:

* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}

== Top Halters ==
The current top 10 BB(3,3) halters (known by [[User:sligocki|Shawn Ligocki]]) are
<pre>
Standard format Status S Σ
0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC Halt 119112334170342541 374676383
1RB2LA1LC_0LA2RB1LB_1RZ1RA1RC Halt 119112334170342540 374676383
1RB2RC1LA_2LA1RB1RZ_2RB2RA1LC Halt 4345166620336565 95524079
1RB1LA2LC_2LA2RB1RB_1RZ0LB0RC Halt 452196003014837 21264944
1RB1RZ2LC_1LC2RB1LB_1LA2RC2LA Halt 4144465135614 2950149
1RB2LA1RA_1RC2RB0RC_1LA1RZ1LA Halt 987522842126 1525688
1RB1RZ2RB_1LC0LB1RA_1RA2LC1RC Halt 4939345068 107900
1RB2LA1RA_1LB1LA2RC_1RZ1LC2RB Halt 1808669066 43925
1RB2LA1RA_1LC1LA2RC_1RZ1LA2RB Halt 1808669046 43925
1RB2LA1RA_1LB1LA2RC_1RZ1LA2RB Halt 1808669046 43925
</pre>
Numbers listed are step count and sigma score for each TM. For a longer list of halting TMs see https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/3x3. For historical perspective see Pascal Michel's [https://bbchallenge.org/~pascal.michel/ha#tm33 '''Historical survey of Busy Beavers'''].

== Certified Progress ==
On [https://discord.com/channels/960643023006490684/1259770474897080380/1325592156257124443 5 Jan 2025], @tjligocki finished an enumeration and filtering of the BB(3,3) machines using the established Ligocki filters, listing the filter used for each machine. He also computed the number of steps and sigma scores for all found halting TMs. The thorough results are located [https://drive.google.com/drive/folders/101U9htddFdE889agAZnU58VLgQJlfn0v?usp=drive_link here]. 367 machines remained on that list. These results were updated on [https://discord.com/channels/960643023006490684/1259770474897080380/1352398469456859167 20 Mar 2025] in the same location and 76 machines remained on the list.

Over two-thirds of the 367 remaining machines were shown to be non-halting with FAR and MITMWFAR by @Justin Blanchard on [https://discord.com/channels/960643023006490684/1259770474897080380/1262265485639286876 14 July 2024]. Most of the remainders were shown non-halting by @lijil on [https://discord.com/channels/960643023006490684/1084047886494470185/1116351783040716830 8 June 2023.] Together, this leaves 21 unsolved TMs, all of which were on @Justin Blanchard's informal holdouts list of 22 machines (see below). The extra machine on Justin's list {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} had been solved by @lijil before, but this was not realized for some time.

On [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 26 Feb 2025], @mxdys published a list of 19 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @Justin Blanchard's June 2024 informal [[Holdouts lists|holdouts list]] of 22 TMs.

=== Cryptids ===
* 829: Bigfoot: {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}

=== Unsolved ===
* {{TM|1RB1LB2LC_1LA2RB1RB_---0LA2LA|undecided}} (397)
* {{TM|1RB0LB0RC_2LC2LA1RA_1RA1LC---|undecided}} (153, equivalent to 758)
* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}} (758, equivalent to 153)
* Wily Coyote: {{TM|1RB2LA1LA_2LA0RA2RC_---0LC2RA|undecided}} (531, equivalent to 532)
* {{TM|1RB2LA1LA_2LA0RA2RC_---1RB2RA|undecided}} (532, equivalent to 531)

=== Solved with moderate rigor ===
* {{TM|1RB2LA1LC_1LA2RB1RB_---2LB0LC|undecided}} (543). See argument for non-halting by @dyuan on [https://discord.com/channels/960643023006490684/1084047886494470185/1240854539519791216 16 May 2024] and [https://discord.com/channels/960643023006490684/1259770474897080380/1325646208483590177 5 January 2025.]
* {{TM|1RB1LC1LC_1LA2RB0RB_2LB---0LA|undecided}} (412) ([https://cosearch.bbchallenge.org/contribution/f9gdw0mg cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1279055891559223399 Longitudinal analysis by @Legion implies non-halting.]
* {{TM|1RB2LB0LC_2LA2RA1RB_---2LA1LC|undecided}} (650) ([https://cosearch.bbchallenge.org/contribution/32099ui7 cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1290044219481657476 Longitudinal analysis (with extra typo disclaimer) by @Legion implies non-halting.]

* {{TM|1RB0RC---_2RC0LB1LB_2LC2RA2RB|undecided}} (279). [https://discord.com/channels/960643023006490684/1084047886494470185/1256729514076016733 Longitudinal analysis by @Legion implies non-halting.]
* {{TM|1RB2RB1LC_1LA2RB0RB_2LB---0LA|undecided}} (867). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting.]

=== Formally proven ===
* {{TM|1RB1LC---_0LC2RB1LB_2LA0RC1RC|undecided}} (400, equivalent to 494). [https://discord.com/channels/960643023006490684/1218877181321678928/1265131102289264690 Coq proof by @-d.] [https://discord.com/channels/960643023006490684/1084047886494470185/1215532512307052634 Equivalence argument provided by @Legion.]

* {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} (494, equivalent to 400, non-halting certified on @lijil's list, equivalence not certified)
* {{TM|1RB2LA2RA_1LC1LB0RA_2RA0LB---|undecided}} (637) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys.] Analyzed by [https://discord.com/channels/960643023006490684/1084047886494470185/1211655096098885732 @Justin,] proven by [https://discord.com/channels/960643023006490684/1084047886494470185/1222028527755460700 @dyuan] and [https://discord.com/channels/960643023006490684/1259770474897080380/1327101773604720730 @Andrew.]
* {{TM|1RB2LB---_1RC2RB1LC_0LA0RB1LB|undecided}} (642, related to Group 1) ([https://cosearch.bbchallenge.org/contribution/3wxkcx6f cosearch]). Coq proof by @-d. [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan.
* {{TM|1RB2RB---_1LC2LB1RC_0RA0LB1RB|undecided}} (834) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys.] [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan, who noted a similarity to 642.
The following TMs were Coq-decided individually [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 by mxdys,] but analysis beforehand showed their halting problems were highly dependent on that of machine 816. If it was non-halting, then 21, 92, 683, 817, and 818 were all non-halting. If 816 halted via transition C0, then 817 halted. And if 816 halted via transition C2, then 21, 92, 683 and 818 all halted. A compilation of the various analyses can be found [https://discord.com/channels/960643023006490684/1259770474897080380/1291694606534049793 here.]
* {{TM|1RB---0LC_2LC2RC1LB_0RA2RB0LB|undecided}} (21, equivalent to 92 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting.]
* {{TM|1RB---1RB_2LC2RC1LB_0RA2RB0LB|undecided}} (92, equivalent to 21 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1213612098232262707 Equivalence claim to 21 by @dyuan1.]
* {{TM|1RB2LC---_0LA0RC1LC_1RB2RC1LB|undecided}} (683)
* {{TM|1RB2RA1LB_0LC0RA1LA_---2LA---|undecided}} (816). [https://discord.com/channels/960643023006490684/1259770474897080380/1278398402450817025 See discussion] of likely non-halting by @Rae and @Peacemaker on 28 August 2024.
* {{TM|1RB2RA1LB_0LC0RA1LA_---2RB2LA|undecided}} (817)
* {{TM|1RB2RA1LB_0LC0RA1LA_2LA0RB---|undecided}} (818, equivalent to 21 and 92)
[[Category:BB Domain]]

BB(3,3)

2025-05-17T11:21:26Z

Fr tho: Update

The 3-state, 3-symbol Busy Beaver problem '''BB(3,3)''' is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Bigfoot]] in 2023, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(3,3) and thus [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3,3) is Hard].

The current BB(3,3) champion {{TM|0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC|halt}} was discovered by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in 2007, proving the lower bounds:

<math display="block">\begin{array}{lcrl}
S(3, 3) & \ge & 119{,}112{,}334{,}170{,}342{,}541 & > 10^{17} \\
\Sigma(3, 3) & \ge & 374{,}676{,}383 & > 10^8 \\
\end{array}</math>

One of the 6 currently unsolved TMs, {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}, is under very active exploration in channel #bb3x3 and believed to be a [[probviously]] halting TM by some members. If it halts, it will be the new champion.

== Cryptids ==
Known BB(3,3) Cryptids:
* {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}, known as [[Bigfoot]]
Possibly probviously halting Cryptid:

* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}}

== Top Halters ==
The current top 10 BB(3,3) halters (known by [[User:sligocki|Shawn Ligocki]]) are
<pre>
0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC Halt 119112334170342541 374676383
1RB2LA1LC_0LA2RB1LB_1RZ1RA1RC Halt 119112334170342540 374676383
1RB2RC1LA_2LA1RB1RZ_2RB2RA1LC Halt 4345166620336565 95524079
1RB1LA2LC_2LA2RB1RB_1RZ0LB0RC Halt 452196003014837 21264944
1RB1RZ2LC_1LC2RB1LB_1LA2RC2LA Halt 4144465135614 2950149
1RB2LA1RA_1RC2RB0RC_1LA1RZ1LA Halt 987522842126 1525688
1RB1RZ2RB_1LC0LB1RA_1RA2LC1RC Halt 4939345068 107900
1RB2LA1RA_1LB1LA2RC_1RZ1LC2RB Halt 1808669066 43925
1RB2LA1RA_1LC1LA2RC_1RZ1LA2RB Halt 1808669046 43925
1RB2LA1RA_1LB1LA2RC_1RZ1LA2RB Halt 1808669046 43925
</pre>
Numbers listed are step count and sigma score for each TM. For a longer list of halting TMs see https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/3x3. For historical perspective see Pascal Michel's [https://bbchallenge.org/~pascal.michel/ha#tm33 '''Historical survey of Busy Beavers'''].

== Certified Progress ==
On [https://discord.com/channels/960643023006490684/1259770474897080380/1325592156257124443 5 Jan 2025], @tjligocki finished an enumeration and filtering of the BB(3,3) machines using the established Ligocki filters, listing the filter used for each machine. He also computed the number of steps and sigma scores for all found halting TMs. The thorough results are located [https://drive.google.com/drive/folders/101U9htddFdE889agAZnU58VLgQJlfn0v?usp=drive_link here]. 367 machines remained on that list. These results were updated on [https://discord.com/channels/960643023006490684/1259770474897080380/1352398469456859167 20 Mar 2025] in the same location and 76 machines remained on the list.

Over two-thirds of the 367 remaining machines were shown to be non-halting with FAR and MITMWFAR by @Justin Blanchard on [https://discord.com/channels/960643023006490684/1259770474897080380/1262265485639286876 14 July 2024]. Most of the remainders were shown non-halting by @lijil on [https://discord.com/channels/960643023006490684/1084047886494470185/1116351783040716830 8 June 2023.] Together, this leaves 21 unsolved TMs, all of which were on @Justin Blanchard's informal holdouts list of 22 machines (see below). The extra machine on Justin's list {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} had been solved by @lijil before, but this was not realized for some time.

On [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 26 Feb 2025], @mxdys published a list of 19 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @Justin Blanchard's June 2024 informal [[Holdouts lists|holdouts list]] of 22 TMs.

=== Cryptids ===
* 829: Bigfoot: {{TM|1RB2RA1LC_2LC1RB2RB_---2LA1LA|undecided}}

=== Unsolved ===
* {{TM|1RB1LB2LC_1LA2RB1RB_---0LA2LA|undecided}} (397)
* {{TM|1RB0LB0RC_2LC2LA1RA_1RA1LC---|undecided}} (153, equivalent to 758)
* {{TM|1RB2LC1RC_2LC---2RB_2LA0LB0RA|undecided}} (758, equivalent to 153)
* Wily Coyote: {{TM|1RB2LA1LA_2LA0RA2RC_---0LC2RA|undecided}} (531, equivalent to 532)
* {{TM|1RB2LA1LA_2LA0RA2RC_---1RB2RA|undecided}} (532, equivalent to 531)

=== Solved with moderate rigor ===
* {{TM|1RB2LA1LC_1LA2RB1RB_---2LB0LC|undecided}} (543). See argument for non-halting by @dyuan on [https://discord.com/channels/960643023006490684/1084047886494470185/1240854539519791216 16 May 2024] and [https://discord.com/channels/960643023006490684/1259770474897080380/1325646208483590177 5 January 2025.]
* {{TM|1RB1LC1LC_1LA2RB0RB_2LB---0LA|undecided}} (412) ([https://cosearch.bbchallenge.org/contribution/f9gdw0mg cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1279055891559223399 Longitudinal analysis by @Legion implies non-halting.]
* {{TM|1RB2LB0LC_2LA2RA1RB_---2LA1LC|undecided}} (650) ([https://cosearch.bbchallenge.org/contribution/32099ui7 cosearch]). [https://discord.com/channels/960643023006490684/1259770474897080380/1290044219481657476 Longitudinal analysis (with extra typo disclaimer) by @Legion implies non-halting.]

* {{TM|1RB0RC---_2RC0LB1LB_2LC2RA2RB|undecided}} (279). [https://discord.com/channels/960643023006490684/1084047886494470185/1256729514076016733 Longitudinal analysis by @Legion implies non-halting.]
* {{TM|1RB2RB1LC_1LA2RB0RB_2LB---0LA|undecided}} (867). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting.]

=== Formally proven ===
* {{TM|1RB1LC---_0LC2RB1LB_2LA0RC1RC|undecided}} (400, equivalent to 494). [https://discord.com/channels/960643023006490684/1218877181321678928/1265131102289264690 Coq proof by @-d.] [https://discord.com/channels/960643023006490684/1084047886494470185/1215532512307052634 Equivalence argument provided by @Legion.]

* {{TM|1RB2LA0LA_2LC---2RA_0RA2RC1LC|undecided}} (494, equivalent to 400, non-halting certified on @lijil's list, equivalence not certified)
* {{TM|1RB2LA2RA_1LC1LB0RA_2RA0LB---|undecided}} (637) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys.] Analyzed by [https://discord.com/channels/960643023006490684/1084047886494470185/1211655096098885732 @Justin,] proven by [https://discord.com/channels/960643023006490684/1084047886494470185/1222028527755460700 @dyuan] and [https://discord.com/channels/960643023006490684/1259770474897080380/1327101773604720730 @Andrew.]
* {{TM|1RB2LB---_1RC2RB1LC_0LA0RB1LB|undecided}} (642, related to Group 1) ([https://cosearch.bbchallenge.org/contribution/3wxkcx6f cosearch]). Coq proof by @-d. [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan.
* {{TM|1RB2RB---_1LC2LB1RC_0RA0LB1RB|undecided}} (834) [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 Coq-decided by @mxdys.] [https://discord.com/channels/960643023006490684/1084047886494470185/1222694817771814922 See argument] for non-halting by @dyuan, who noted a similarity to 642.
The following TMs were Coq-decided individually [https://discord.com/channels/960643023006490684/1259770474897080380/1344554618188730368 by mxdys,] but analysis beforehand showed their halting problems were highly dependent on that of machine 816. If it was non-halting, then 21, 92, 683, 817, and 818 were all non-halting. If 816 halted via transition C0, then 817 halted. And if 816 halted via transition C2, then 21, 92, 683 and 818 all halted. A compilation of the various analyses can be found [https://discord.com/channels/960643023006490684/1259770474897080380/1291694606534049793 here.]
* {{TM|1RB---0LC_2LC2RC1LB_0RA2RB0LB|undecided}} (21, equivalent to 92 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1256634331464601640 Longitudinal analysis by @Legion implies non-halting.]
* {{TM|1RB---1RB_2LC2RC1LB_0RA2RB0LB|undecided}} (92, equivalent to 21 and 818). [https://discord.com/channels/960643023006490684/1084047886494470185/1213612098232262707 Equivalence claim to 21 by @dyuan1.]
* {{TM|1RB2LC---_0LA0RC1LC_1RB2RC1LB|undecided}} (683)
* {{TM|1RB2RA1LB_0LC0RA1LA_---2LA---|undecided}} (816). [https://discord.com/channels/960643023006490684/1259770474897080380/1278398402450817025 See discussion] of likely non-halting by @Rae and @Peacemaker on 28 August 2024.
* {{TM|1RB2RA1LB_0LC0RA1LA_---2RB2LA|undecided}} (817)
* {{TM|1RB2RA1LB_0LC0RA1LA_2LA0RB---|undecided}} (818, equivalent to 21 and 92)
[[Category:BB Domain]]

BB(2,5)

2025-05-17T11:16:18Z

Fr tho: Fix

The 2-state, 5-symbol Busy Beaver problem '''BB(2,5)''' is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Hydra]] by Daniel Yuan in April 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(2,5) and thus [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2,5) is Hard].

The current BB(2,5) champion is {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}}, also discovered by Daniel Yuan in June 2024. It is a halting [[shift overflow counter]], and is in fact the only known champion machine that exhibits [[Counter]] behavior. It provides the lower bound:

<math display="block">S(2,5) > \Sigma(2,5) > 10^{10^{10^{3\,314\,360}}} > 10 \uparrow\uparrow 4</math>

== Cryptids ==
Known BB(2,5) Cryptids

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA}}, known as [[Hydra]].
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB}}, known as the bonus cryptid

== Certified progress ==
In April 2024, Shawn Ligocki publicly released a list of 23,411 undecided BB(2,5) machines. Justin Blanchard then made substantial progress over the course of the next month, reducing the list to 499 holdouts by late May 2024. In June 2024, @mxdys cut down the list to 273 using halting and inductive deciders, and again to 217 using [[Closed Tape Language (CTL)|CTL]]. In February 2025, @mxdys ran a decider pipeline in Coq that resulted in only 173 holdouts. Since then, additional machines have been proven in Coq using both deciders and individual proofs.

On 29 Mar 2025, @mxdys published a list of 83 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @mxdys's March 2025 holdout list of 83 TMs.

=== Cryptids ===

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA|undecided}}. Hydra
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB|undecided}}. Bonus cryptid

=== Unsolved ===

* {{TM|1RB---4LB1RA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---4LB0LA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}. [https://discord.com/channels/960643023006490684/1354037062830919690/1354037062830919690 Shift overflow counter, potential cryptid]
* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}. Potential cryptid
* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}. Potential cryptid
* {{TM|1RB3LA1LA4LA2RA_2LB2RA---0RA0RB|undecided}}.
* {{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|undecided}}.
* {{TM|1RB---3RA2LA2RB_2LB3LA4LB4RA0RA|undecided}}.
* {{TM|1RB4LA1RA1RB1LA_2LB3LA---4RA2RB|undecided}}. BMO 3 variant?
* {{TM|1RB---4RB2RB4LA_2LB3LA3LB0RA0RB|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353983911222312970 Bouncer + chaotic counter]
* {{TM|1RB2RB3LA4LA1LA_2LB3RA---4RA1RB|undecided}}.
* {{TM|1RB3RB3LA4LA2RB_2LB3RA---1RA1LA|undecided}}.
* {{TM|1RB2LA4LA1RA1LA_2LB3RB4RB---2RA|undecided}}.
* {{TM|1RB4RB4RA1LA3LA_1LB2LA3RB2RB---|undecided}}.
* {{TM|1RB3RA3RB4LA1LA_1LB2LA1LA---1RB|undecided}}. [https://discord.com/channels/960643023006490684/1349602897024782358 Potentially halt]
* {{TM|1RB2RA4LA1RB4RB_1LB2LA3RA---0LB|undecided}}.
* {{TM|1RB3RB1LA2LA3RA_1LB2RA4RB0LA---|undecided}}.
* {{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}.
* {{TM|1RB2LA0RB0LB3LB_2LA4RB3RA0RA---|undecided}}.
* {{TM|1RB2RA3LB---2LB_2LA0LA4RB0RB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329808777754706046 30% chance of beating current champion]
* {{TM|1RB2RA3LB4LA---_2LA0RB1LA2RB0RA|undecided}}. [https://discord.com/channels/960643023006490684/1348878717870673981 Analysis by @dyuan01 and @Legion]
* {{TM|1RB2RA3LA---2LB_2LA4RA4RB0RB0LA|undecided}}. Spaghetti [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 analysis by @nerdyjoe]
* {{TM|1RB2RA3LA4LA2RB_2LA---3LB1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1355112650690003028 Bouncer + chaotic counter]
* {{TM|1RB2RA3LA4LA2RB_2LA3RB---0RA1LA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA1RA4LA2RA_2LA---1LA0RA3RB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA3LB0RB0LA_2LA4RB1LB1RA---|undecided}}.
* {{TM|1RB3LA1LA2RB2RA_2LA4RA3LB1RA---|undecided}}.
* {{TM|1RB3LA3LA0RB2LB_2LA4LA4RA2RA---|undecided}}.
* {{TM|1RB3RA2LB1LB1RB_2LA2RA4LA1LA—--|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RA4LB2RA2RB_2LA---3LA0LB1LA|undecided}}.
* {{TM|1RB0LB2LA4LB3LA_2LA---3RA4RB2RB|undecided}}.
* {{TM|1RB2LB3LA0RA1LB_2LA4RA3RB3LA---|undecided}}. [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 Analysis by @nerdyjoe]
* {{TM|1RB2RB---0LB3LA_2LA2LB3RB4RB1LB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB2RB4LA2RA1LA_2LA4RA3LA---3RA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353987502062702622 Longitudinal analysis suggests chaotic]
* {{TM|1RB3LB0RB---2LB_2LA3RA4RB2RB0LA|undecided}}.
* {{TM|1RB3LB4LA0LB---_2LA0LA1RB0RA3RA|undecided}}.
* {{TM|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RB---4RA2RA_2LA2RA3LB4LB1LB|undecided}}.
* {{TM|1RB3RB---0RA2RB_2LA4RA3LB1LB1LA|undecided}}.
* {{TM|1RB3RB1LB2RA---_2LA2RB1LA4LB0RA|undecided}}.
* {{TM|1RB2LA1RA---1LA_1LA4RB3LB0RB2RB|undecided}}. Fractal?
* {{TM|1RB2LA3LA4RA0LA_1LA3RB1RB1LB---|undecided}}. Fractal?
* {{TM|1RB2LA0RB1LA3LB_1LA3LB1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB4LB1RA_1LA3RA1RA---0LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4RB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB3RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LA|undecided}}.
* {{TM|1RB2LA0RB1LB0LB_1LA3RA1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB---4LA_1LA3LA1RA4RA1LB|undecided}}.
* {{TM|1RB2LA0RB4LB0LA_1LA3LA1RA4RA---|undecided}}.
* {{TM|1RB2LA4RA1LA3LA_0LA2RB3RB2LB---|undecided}}. 1D CA-like
* {{TM|1RB2LA4RA1LA3LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA1LA4RA2LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA3LA4RA1LA_0LA3LB3RB1RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA0LB1LA2RA_0LA3RA1RA4LB—--|undecided}}. Potential bouncer
* {{TM|1RB2LA3LB4LB---_0LA4LB3RA4LA0RB|undecided}}. Fractal?

=== Solved with moderate rigor ===

* {{TM|1RB1RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB0RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB4LA1LB2LA0RB_2LB3RB4LA---1RA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 Nonhalting argument by @dyuan]
* {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---|undecided}}. Current champion
* {{TM|1RB2RA3LA4RB---_2LA3RB3RA1LB3LB|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1256293368909004820 Counter] that halts in at most 56452325275 steps
* {{TM|1RB2RA3LA4LA2RB_2LA---1LA1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA1LA2RA_2LA4RB---0RA0LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA2RB1LA_2LA4RB---3RA3LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB2LB---4LB0RB_1LA3RB4RB4RA1LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Nonhalting argument by @racheline]

=== Formally proven ===

* {{TM|1RB2RA3LA4LA2RB_2LA0RA---0RA1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]

[[Category:BB Domain]]

BB(2,5)

2025-05-17T11:13:06Z

Fr tho: Change to TM template

The 2-state, 5-symbol Busy Beaver problem '''BB(2,5)''' is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Hydra]] by Daniel Yuan in April 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(2,5) and thus [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2,5) is Hard].

The current BB(2,5) champion is {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}}, also discovered by Daniel Yuan in June 2024. It is a halting [[shift overflow counter]], and is in fact the only known champion machine that exhibits [[Counter]] behavior. It provides the lower bound:

<math display="block">S(2,5) > \Sigma(2,5) > 10^{10^{10^{3\,314\,360}}} > 10 \uparrow\uparrow 4</math>

== Cryptids ==
Known BB(2,5) Cryptids

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA}}, known as [[Hydra]].
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB}}, known as the bonus cryptid

== Certified progress ==
In April 2024, Shawn Ligocki publicly released a list of 23,411 undecided BB(2,5) machines. Justin Blanchard then made substantial progress over the course of the next month, reducing the list to 499 holdouts by late May 2024. In June 2024, @mxdys cut down the list to 273 using halting and inductive deciders, and again to 217 using [[Closed Tape Language (CTL)|CTL]]. In February 2025, @mxdys ran a decider pipeline in Coq that resulted in only 173 holdouts. Since then, additional machines have been proven in Coq using both deciders and individual proofs.

On 29 Mar 2025, @mxdys published a list of 83 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @mxdys's March 2025 holdout list of 83 TMs.

=== Cryptids ===

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA|undecided}}. Hydra
* 1RB3RB---3LA1RA_2LA3RA4LB0LB1LB|undecided}}. Bonus cryptid

=== Unsolved ===

* {{TM|1RB---4LB1RA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---4LB0LA4RA_2LB2LA3RA4LB0RB|undecided}}.
* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}. [https://discord.com/channels/960643023006490684/1354037062830919690/1354037062830919690 Shift overflow counter, potential cryptid]
* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}. Potential cryptid
* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}. Potential cryptid
* {{TM|1RB3LA1LA4LA2RA_2LB2RA---0RA0RB|undecided}}.
* {{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|undecided}}.
* {{TM|1RB---3RA2LA2RB_2LB3LA4LB4RA0RA|undecided}}.
* {{TM|1RB4LA1RA1RB1LA_2LB3LA---4RA2RB|undecided}}. BMO 3 variant?
* {{TM|1RB---4RB2RB4LA_2LB3LA3LB0RA0RB|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353983911222312970 Bouncer + chaotic counter]
* {{TM|1RB2RB3LA4LA1LA_2LB3RA---4RA1RB|undecided}}.
* {{TM|1RB3RB3LA4LA2RB_2LB3RA---1RA1LA|undecided}}.
* {{TM|1RB2LA4LA1RA1LA_2LB3RB4RB---2RA|undecided}}.
* {{TM|1RB4RB4RA1LA3LA_1LB2LA3RB2RB---|undecided}}.
* {{TM|1RB3RA3RB4LA1LA_1LB2LA1LA---1RB|undecided}}. [https://discord.com/channels/960643023006490684/1349602897024782358 Potentially halt]
* {{TM|1RB2RA4LA1RB4RB_1LB2LA3RA---0LB|undecided}}.
* {{TM|1RB3RB1LA2LA3RA_1LB2RA4RB0LA---|undecided}}.
* {{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}.
* {{TM|1RB2LA0RB0LB3LB_2LA4RB3RA0RA---|undecided}}.
* {{TM|1RB2RA3LB---2LB_2LA0LA4RB0RB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329808777754706046 30% chance of beating current champion]
* {{TM|1RB2RA3LB4LA---_2LA0RB1LA2RB0RA|undecided}}. [https://discord.com/channels/960643023006490684/1348878717870673981 Analysis by @dyuan01 and @Legion]
* {{TM|1RB2RA3LA---2LB_2LA4RA4RB0RB0LA|undecided}}. Spaghetti [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 analysis by @nerdyjoe]
* {{TM|1RB2RA3LA4LA2RB_2LA---3LB1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1355112650690003028 Bouncer + chaotic counter]
* {{TM|1RB2RA3LA4LA2RB_2LA3RB---0RA1LA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA1RA4LA2RA_2LA---1LA0RA3RB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LA3LB0RB0LA_2LA4RB1LB1RA---|undecided}}.
* {{TM|1RB3LA1LA2RB2RA_2LA4RA3LB1RA---|undecided}}.
* {{TM|1RB3LA3LA0RB2LB_2LA4LA4RA2RA---|undecided}}.
* {{TM|1RB3RA2LB1LB1RB_2LA2RA4LA1LA—--|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RA4LB2RA2RB_2LA---3LA0LB1LA|undecided}}.
* {{TM|1RB0LB2LA4LB3LA_2LA---3RA4RB2RB|undecided}}.
* {{TM|1RB2LB3LA0RA1LB_2LA4RA3RB3LA---|undecided}}. [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 Analysis by @nerdyjoe]
* {{TM|1RB2RB---0LB3LA_2LA2LB3RB4RB1LB|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB2RB4LA2RA1LA_2LA4RA3LA---3RA|undecided}}. Longitudinal analysis suggests chaotic
* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353987502062702622 Longitudinal analysis suggests chaotic]
* {{TM|1RB3LB0RB---2LB_2LA3RA4RB2RB0LA|undecided}}.
* {{TM|1RB3LB4LA0LB---_2LA0LA1RB0RA3RA|undecided}}.
* {{TM|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* {{TM|1RB3RB---4RA2RA_2LA2RA3LB4LB1LB|undecided}}.
* {{TM|1RB3RB---0RA2RB_2LA4RA3LB1LB1LA|undecided}}.
* {{TM|1RB3RB1LB2RA---_2LA2RB1LA4LB0RA|undecided}}.
* {{TM|1RB2LA1RA---1LA_1LA4RB3LB0RB2RB|undecided}}. Fractal?
* {{TM|1RB2LA3LA4RA0LA_1LA3RB1RB1LB---|undecided}}. Fractal?
* {{TM|1RB2LA0RB1LA3LB_1LA3LB1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB4LB1RA_1LA3RA1RA---0LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4RB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LB|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB3RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB2LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB1LA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0RA|undecided}}.
* {{TM|1RB2LA0RB1LB---_1LA3RA1RA4LB0LA|undecided}}.
* {{TM|1RB2LA0RB1LB0LB_1LA3RA1RA4RA---|undecided}}.
* {{TM|1RB2LA0RB---4LA_1LA3LA1RA4RA1LB|undecided}}.
* {{TM|1RB2LA0RB4LB0LA_1LA3LA1RA4RA---|undecided}}.
* {{TM|1RB2LA4RA1LA3LA_0LA2RB3RB2LB---|undecided}}. 1D CA-like
* {{TM|1RB2LA4RA1LA3LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA1LA4RA2LA_0LA3RB3LB2RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA3LA4RA1LA_0LA3LB3RB1RB---|undecided}}. 1D CA-like
* {{TM|1RB2LA0LB1LA2RA_0LA3RA1RA4LB—--|undecided}}. Potential bouncer
* {{TM|1RB2LA3LB4LB---_0LA4LB3RA4LA0RB|undecided}}. Fractal?

=== Solved with moderate rigor ===

* {{TM|1RB1RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB0RB3LA4LA2RA_2LB3RA---3RA4RB|undecided}}. BMO problem 3
* {{TM|1RB4LA1LB2LA0RB_2LB3RB4LA---1RA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 Nonhalting argument by @dyuan]
* {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---|undecided}}. Current champion
* {{TM|1RB2RA3LA4RB---_2LA3RB3RA1LB3LB|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1256293368909004820 Counter] that halts in at most 56452325275 steps
* {{TM|1RB2RA3LA4LA2RB_2LA---1LA1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA1LA2RA_2LA4RB---0RA0LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB3LA4LA2RB1LA_2LA4RB---3RA3LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* {{TM|1RB2LB---4LB0RB_1LA3RB4RB4RA1LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Nonhalting argument by @racheline]

=== Formally proven ===

* {{TM|1RB2RA3LA4LA2RB_2LA0RA---0RA1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]

[[Category:BB Domain]]

BB(2,5)

2025-05-17T10:59:29Z

Fr tho: WIP

The 2-state, 5-symbol Busy Beaver problem '''BB(2,5)''' is unsolved. With the discovery of the [[Cryptids|Cryptid]] machine [[Hydra]] by Daniel Yuan in April 2024, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(2,5) and thus [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2,5) is Hard].

The current BB(2,5) champion is {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}}, also discovered by Daniel Yuan in June 2024. It is a halting [[shift overflow counter]], and is in fact the only known champion machine that exhibits [[Counter]] behavior. It provides the lower bound:

<math display="block">S(2,5) > \Sigma(2,5) > 10^{10^{10^{3\,314\,360}}} > 10 \uparrow\uparrow 4</math>

== Cryptids ==
Known BB(2,5) Cryptids

* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA}}, known as [[Hydra]].
* {{TM|1RB3RB---3LA1RA_2LA3RA4LB0LB1LB}}, known as the bonus cryptid

== Certified progress ==
In April 2024, Shawn Ligocki publicly released a list of 23,411 undecided BB(2,5) machines. Justin Blanchard then made substantial progress over the course of the next month, reducing the list to 499 holdouts by late May 2024. In June 2024, @mxdys cut down the list to 273 using halting and inductive deciders, and again to 217 using [[Closed Tape Language (CTL)|CTL]]. In February 2025, @mxdys ran a decider pipeline in Coq that resulted in only 173 holdouts. Since then, additional machines have been proven in Coq using both deciders and individual proofs.

On 29 Mar 2025, @mxdys published a list of 83 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

== Holdouts ==
This section is based on @mxdys's March 2025 holdout list of 83 TMs.

=== Cryptids ===

* [[Hydra|1RB3RB---3LA1RA_2LA3RA4LB0LB0LA]] Hydra
* 1RB3RB---3LA1RA_2LA3RA4LB0LB1LB Bonus cryptid

=== Unsolved ===

* 1RB---4LB1RA4RA_2LB2LA3RA4LB0RB
* 1RB---4LB0LA4RA_2LB2LA3RA4LB0RB
* 1RB---0RB0LA2RA_2LB2LA3RA4LB0LB [https://discord.com/channels/960643023006490684/1354037062830919690/1354037062830919690 Shift overflow counter, potential cryptid]
* [[1RB3LA1LA1RA3RA_2LB2RA---4RB1LB]] Potential cryptid
* [[1RB3LA1LA1RA1RA_2LB2RA---4RB1LB]] Potential cryptid
* 1RB3LA1LA4LA2RA_2LB2RA---0RA0RB
* 1RB4RA1LA4RB2LA_2LB3LA1RB2RA---
* 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA
* 1RB4LA1RA1RB1LA_2LB3LA---4RA2RB BMO 3 variant?
* 1RB---4RB2RB4LA_2LB3LA3LB0RA0RB [https://discord.com/channels/960643023006490684/1353983911222312970/1353983911222312970 Bouncer + chaotic counter]
* 1RB2RB3LA4LA1LA_2LB3RA---4RA1RB
* 1RB3RB3LA4LA2RB_2LB3RA---1RA1LA
* 1RB2LA4LA1RA1LA_2LB3RB4RB---2RA
* 1RB4RB4RA1LA3LA_1LB2LA3RB2RB---
* 1RB3RA3RB4LA1LA_1LB2LA1LA---1RB [https://discord.com/channels/960643023006490684/1349602897024782358 Potentially halt]
* 1RB2RA4LA1RB4RB_1LB2LA3RA---0LB
* 1RB3RB1LA2LA3RA_1LB2RA4RB0LA---
* 1RB3LA1LA2RB2LB_1LB2RA4RA0RB---
* 1RB2LA0RB0LB3LB_2LA4RB3RA0RA---
* 1RB2RA3LB---2LB_2LA0LA4RB0RB1LA [https://discord.com/channels/960643023006490684/1259770421046411285/1329808777754706046 30% chance of beating current champion]
* 1RB2RA3LB4LA---_2LA0RB1LA2RB0RA [https://discord.com/channels/960643023006490684/1348878717870673981 Analysis by @dyuan01 and @Legion]
* 1RB2RA3LA---2LB_2LA4RA4RB0RB0LA Spaghetti [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 analysis by @nerdyjoe]
* 1RB2RA3LA4LA2RB_2LA---3LB1RA3RA [https://discord.com/channels/960643023006490684/1353983911222312970/1355112650690003028 Bouncer + chaotic counter]
* 1RB2RA3LA4LA2RB_2LA3RB---0RA1LA Longitudinal analysis suggests chaotic
* 1RB3LA1RA4LA2RA_2LA---1LA0RA3RB Longitudinal analysis suggests chaotic
* 1RB3LA3LB0RB0LA_2LA4RB1LB1RA---
* 1RB3LA1LA2RB2RA_2LA4RA3LB1RA---
* 1RB3LA3LA0RB2LB_2LA4LA4RA2RA---
* 1RB3RA2LB1LB1RB_2LA2RA4LA1LA— [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* 1RB3RA4LB2RA2RB_2LA---3LA0LB1LA
* 1RB0LB2LA4LB3LA_2LA---3RA4RB2RB
* 1RB2LB3LA0RA1LB_2LA4RA3RB3LA--- [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 Analysis by @nerdyjoe]
* 1RB2RB---0LB3LA_2LA2LB3RB4RB1LB Longitudinal analysis suggests chaotic
* 1RB2RB4LA2RA1LA_2LA4RA3LA---3RA Longitudinal analysis suggests chaotic
* 1RB3LB---4LA1RB_2LA4LA4LB3RB1RA [https://discord.com/channels/960643023006490684/1353983911222312970/1353987502062702622 Longitudinal analysis suggests chaotic]
* 1RB3LB0RB---2LB_2LA3RA4RB2RB0LA
* 1RB3LB4LA0LB---_2LA0LA1RB0RA3RA
* 1RB3RB1LB---2RB_2LA1RA4LB2LA2RA [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
* 1RB3RB---4RA2RA_2LA2RA3LB4LB1LB
* 1RB3RB---0RA2RB_2LA4RA3LB1LB1LA
* 1RB3RB1LB2RA---_2LA2RB1LA4LB0RA
* 1RB2LA1RA---1LA_1LA4RB3LB0RB2RB Fractal?
* 1RB2LA3LA4RA0LA_1LA3RB1RB1LB--- Fractal?
* 1RB2LA0RB1LA3LB_1LA3LB1RA4RA---
* 1RB2LA0RB4LB1RA_1LA3RA1RA---0LA
* 1RB2LA0RB1LB---_1LA3RA1RA4RB0LB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB2RB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB2LB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB1RB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB1LB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB0RB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB0LB
* 1RB2LA0RB1LB---_1LA3RA1RA4LB3RA
* 1RB2LA0RB1LB---_1LA3RA1RA4LB2RA
* 1RB2LA0RB1LB---_1LA3RA1RA4LB2LA
* 1RB2LA0RB1LB---_1LA3RA1RA4LB1RA
* 1RB2LA0RB1LB---_1LA3RA1RA4LB1LA
* 1RB2LA0RB1LB---_1LA3RA1RA4LB0RA
* 1RB2LA0RB1LB---_1LA3RA1RA4LB0LA
* 1RB2LA0RB1LB0LB_1LA3RA1RA4RA---
* 1RB2LA0RB---4LA_1LA3LA1RA4RA1LB
* 1RB2LA0RB4LB0LA_1LA3LA1RA4RA---
* 1RB2LA4RA1LA3LA_0LA2RB3RB2LB--- 1D CA-like
* 1RB2LA4RA1LA3LA_0LA3RB3LB2RB--- 1D CA-like
* 1RB2LA1LA4RA2LA_0LA3RB3LB2RB--- 1D CA-like
* 1RB2LA3LA4RA1LA_0LA3LB3RB1RB--- 1D CA-like
* 1RB2LA0LB1LA2RA_0LA3RA1RA4LB— Potential bouncer
* 1RB2LA3LB4LB---_0LA4LB3RA4LA0RB Fractal?

=== Solved with moderate rigor ===

* 1RB1RB3LA4LA2RA_2LB3RA---3RA4RB BMO problem 3
* 1RB0RB3LA4LA2RA_2LB3RA---3RA4RB BMO problem 3
* 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA [https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 Nonhalting argument by @dyuan]
* [[1RB3LA4RB0RB2LA 1LB2LA3LA1RA1RZ|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---]] Current champion
* 1RB2RA3LA4RB---_2LA3RB3RA1LB3LB [https://discord.com/channels/960643023006490684/1084047886494470185/1256293368909004820 Counter] that halts in at most 56452325275 steps
* 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* 1RB3LA4LA1LA2RA_2LA4RB---0RA0LA [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]
* 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Nonhalting argument by @racheline]

=== Formally proven ===

* 1RB2RA3LA4LA2RB_2LA0RA---0RA1LA [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]

[[Category:BB Domain]]