BB(5): Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
VisualWikitext
(Added link to "champions")
 
(12 intermediate revisions by 7 users not shown)
Line 1: Line 1:
'''BB(5)''' refers to the 5<sup>th</sup> 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>  
The 5-state, 2-symbol Busy Beaver problem, '''BB(5)''', refers to the 5<sup>th</sup> 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.
In 2024, BB(5) = 47,176,870 was proven by the [[bbchallenge.org]] massively collaborative research project.
Line 12: Line 12:
* In 1973, Weimann establishes S(5) ≥ 556 and Σ(5) ≥ 40.<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 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 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 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 doing so.<ref name=":0" />
* 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 ===
=== 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>
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 in his [[Busy Beaver Frontier]].<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 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 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 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]].
* 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 ==
<references />
[[Category:BB Domains]]

Latest revision as of 10:36, 11 August 2025

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.

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 in his Busy Beaver Frontier.[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.

Champions

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

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

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

References

  1. ↑ 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. ↑ 2.0 2.1 2.2 Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52
  3. ↑ 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.
  4. ↑ https://docs.bbchallenge.org/other/busy.html
  5. ↑ Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369
  6. ↑ https://bbchallenge.org/method
  7. ↑ https://skelet.ludost.net/bb/index.html
  8. ↑ 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/
  9. ↑ https://bbchallenge.org/story
  10. ↑ https://github.com/ccz181078/Coq-BB5
Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=BB(5)&oldid=3040"