# BB(5)

**BB(5)** refers to the 5^{th} 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.^{[1]}

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.
^{[2]} - In 1972, Lynn establishes S(5) ≥ 435 and Σ(5) ≥ 22.
^{[2]} - In 1973, Weimann establishes S(5) ≥ 556 and Σ(5) ≥ 40.
^{[2]} - In 1974, Lynn, cited by Brady (1983)
^{[3]}, establishes S(5) ≥ 7,707 and Σ(5) ≥ 112. - In 1983, the Dortmund contestis 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.
^{[4]} - In 1989, Heiner and Buntrock find the 5-state busy beaver winner, establishing S(5) ≥ 47,176,870 and Σ(5) ≥ 4,098.
^{[1]}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).^{[1]}

### 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.^{[5]} In practice, proving this conjecture requires to study the behavior of ~100 million 5-state machines.^{[6]}

- In 2003, Georgi Georgiev (Skelet) publishes a list of 43 holdouts, based on bbfind, a collection of Deciders written in Pascal.
^{[7]} - In 2009, Joachim Hertel publishes a method claiming 100 holdouts.
^{[8]} - In 2022, bbchallenge.org is released, with the aim of collaboratively proving that BB(5) = 47,176,870.
^{[9]} - In 2024, bbchallenge's contributor @mxdys publishes Coq-BB5, a Coq-verified proof of BB(5) = 47,176,870
^{[10]}, ending a 60 years old quest. This proof uses and/or improves on many other bbchallenge's contributions, see Coq-BB5.

## 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}^{2.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/story
- ↑ https://github.com/ccz181078/Coq-BB5