BB(5)
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.[1]
In 2024, BB(5) = 47,176,870 was proven by the bbchallenge.org massively collaborative research project.[2]
BB(5) is the only BB Domain to have irregular TMs without also having Cryptids.
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 established Σ(5) ≥ 17.[3]
- In 1972, Lynn established S(5) ≥ 435 and Σ(5) ≥ 22.[3]
- In 1973, Weimann established S(5) ≥ 556 and Σ(5) ≥ 40.[3]
- In 1974, Lynn, cited by Brady (1983)[4], established S(5) ≥ 7,707 and Σ(5) ≥ 112.
- In 1983, the Dortmund contest was organised to find new 5-state champions. The winner was Uwe Schult, who established S(5) ≥ 134,467 and Σ(5) ≥ 501.
- In 1984, George Uhing established S(5) ≥ 2,133,492 and Σ(5) ≥ 1,915.[5]
- In 1989, Heiner Marxen and Jürgen Buntrock found a new champion, establishing S(5) ≥ 47,176,870 and Σ(5) ≥ 4,098.[1] They did 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 presented some ideas for automatically deciding the behavior of Turing machines (i.e. making Deciders).[1]
Proving that the 5-state winner is actually the winner
In the decades since 1989, with no new champions discovered, it began to appear that the Marxen-Buntrock champion might be the actual longest running 5-state TM. In 2020, Scott Aaronson formally conjectured that BB(5) = 47,176,870 in his Busy Beaver Frontier.[6] In practice, proving this conjecture requires deciding the behavior of ~100 million 5-state machines.[7]
- In 2003, Georgi Georgiev (Skelet) published a list of 43 holdouts, based on bbfind, a collection of Deciders written in Pascal.[8]
- In 2009, Joachim Hertel published a method claiming 100 holdouts.[9]
- In 2021, all BB(5) TMs were enumerated in TNF[10] and a database of undecided TMs was established.[11]
- In 2022, bbchallenge.org was released, with the aim of collaboratively proving that BB(5) = 47,176,870.[12]
- In 2024, bbchallenge's contributor @mxdys published Coq-BB5, a Rocq-verified proof of BB(5) = 47,176,870[13], ending a 60-year-old quest. This proof uses and/or improves on many other bbchallenge's contributions.
Champions
S(5) = 47,176,870 and there is only one shift champion (in TNF):
1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA(bbch) leaves 4098 ones (a ones champion)
Σ(5) = 4098 and there are 2 ones champions (in TNF):
1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA(bbch) runs for 47,176,870 steps (the steps champion)1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC(bbch) runs for 11,798,826 steps
Top Halters
The top 20 longest running BB(5) TMs (in TNF-1RB) are:
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
For more top halting BB(5) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/5x2
Deciders
All non-halting BB(5) TMs (except for 13 "sporadic" TMs) were decided by the following deciders:
- Cycler, Translated Cycler
- n-Gram CPS
- Repeated Word List (RepWL)
- Finite Automata Reduction (FAR)
- Weighted Finite Automata Reduction (WFAR)
These 13 sporadic TMs were each decided by individual proofs:
- Skelet 1
- Skelet 10
- Skelet 17
- 5 Shift overflow counters (Skelet 15, 26, 33, 34, 35)
- 5 Finned Machines (ex: Finned 3)
See the BB(5) paper[2] for more details.
See also
References
- ↑ 1.0 1.1 1.2 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
- ↑ 2.0 2.1 Determination of the fifth Busy Beaver value. bbchallenge Collaboration et. al. https://arxiv.org/abs/2509.12337
- ↑ 3.0 3.1 3.2 Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52
- ↑ 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.
- ↑ https://docs.bbchallenge.org/other/busy.html
- ↑ Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369
- ↑ https://bbchallenge.org/method
- ↑ https://skelet.ludost.net/bb/index.html
- ↑ 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/
- ↑ https://bbchallenge.org/method#seed-database
- ↑ Downloadable seed database. https://docs.bbchallenge.org/all_5_states_undecided_machines_with_global_header.zip
- ↑ https://bbchallenge.org/story
- ↑ https://github.com/ccz181078/Coq-BB5