BB(5): Difference between revisions

Latest revision as of 14:26, 25 September 2026

The 5-state, 2-symbol Busy Beaver problem, BB(5), refers to the 5^th 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]

The BB(5) champion 1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA (bbch) and a Σ(5) champion 1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC (bbch), were discovered in 1989 by Heiner Marxen and Jürgen Buntrock. These machines were shown to be the definite champions in 2024 by the bbchallenge.org massively collaborative research project^[2], proving:

$\begin{array}{lcrl} BB (5) & = & 47, 176, 870 \\ Σ (5) & = & 4, 098 \end{array}$

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.


Timeline of lower bounds established for Σ(5) and S(5)^[3]
Month of discovery	Machine	S(5) lower bound	Σ(5) lower bound	Discoverer	Notes
?	?	?	≥ 17	?	Mentioned by Green, M., mentioned by Lynn, D.^[4] Step count unknown.
November 1964	`1LD1LB_1LZ1LA_0LB1LD_0LE0LD_1RE1RC` (bbch)	≥ 79	(≥ 13)	Green, M.	Part of an infinite family of machines now known as Green's machines. During this period, the steps champion might have been different to the ones champion.
August 1972	`1RB1RA_1LC0LD_0RA1LB_1RZ0LE_1RC1RB` (bbch)	≥ 435	(≥ 15)	Lynn, D.^[4]	During this period, the steps champion was different to the ones champion. These bounds were published simultaneously.
August 1972	`1RB1RC_1LC1LD_0RA1LB_1RE0LB_1RZ1RD` (bbch)	(≥ 292)	≥ 22	Lynn, D.^[4]
November 1973	`1RB0LD_1RC0RB_1LA0RA_0LC0LE_1LC1RZ` (bbch)	≥ 992	(≥ 23)	Weimann, B.^[5]	During this period, the steps champion was different to the ones champion. These bounds were published simultaneously.
November 1973	`1RB1RA_1RC0RB_1LD1LC_1LE0LC_0RA1RZ` (bbch)	(≥ 556)	≥ 40	Weimann, B.^[5]
1974	`0RB1RZ_1RC0LD_1RD0RE_1LB0LD_1RE1RA` (bbch)	≥ 7,707	(≥ 88)	Lynn, D.^[6]	During this period, the steps champion was different to the ones champion. Bounds were published in 1983. These bounds were published simultaneously.
1974	`1RB0LE_1RC0RA_1LD1RZ_1LE1LD_1LA0LC` (bbch)	(≥ 6,147)	≥ 112	Lynn, D.^[6]
August 1982	`1RB0LC_1RC1RD_1LA0RB_0RE1RZ_1LC1RA` (bbch)	≥ 134,467	≥ 501	Schult, U.^[5]	In 1983, the Dortmund contest was organised to find new 5-state champions; Uwe Schult won with this machine.
December 1984	`1RB1LC_0LA0LD_1LA1RZ_1LB1RE_0RD0RB` (bbch)	≥ 2,133,492	≥ 1,915	Uhing, G.^[7]^[8]	Bound was published by 1985.
February 1986	`1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA` (bbch)	≥ 2,358,064	(≥ 1,471)	Uhing, G.^[7]^[8]	During this period, the steps champion was different to the ones champion.
August 1989	`1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC` (bbch)	≥ 11,798,826	≥ 4,098	Marxen, H., Buntrock, J.^[1]	Eventually proven to be an Σ(5) champion in 2024.
September 1989	`1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB` (bbch)	≥ 23,554,764	(≥ 4,097)		During this period, the steps champion was different to the ones champion.
September 1989	`1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA` (bbch)	≥ 47,176,870	(≥ 4,098)		They did not prove (or claim) that this 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). Eventually proven to be the S(5) champion and an Σ(5) champion in 2024.

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.^[9] In practice, proving this conjecture requires deciding the behavior of ~100 million 5-state machines.^[10]

In 2003, Georgi Georgiev (Skelet) published a list of 43 holdouts, based on bbfind, a collection of Deciders written in Pascal.^[11]
In 2009, Joachim Hertel published a method claiming 100 holdouts.^[12]
In 2021, all BB(5) TMs were enumerated in TNF^[13] and a database of undecided TMs was established.^[14]
In 2022, bbchallenge.org was released, with the aim of collaboratively proving that BB(5) = 47,176,870.^[15]
In 2024, bbchallenge's contributor @mxdys published Coq-BB5, a Rocq-verified proof of BB(5) = 47,176,870^[16], 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:

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.

References

↑ ^1.0 ^1.1 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
↑ Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52
↑ ^4.0 ^4.1 https://docs.bbchallenge.org/papers/Lynn1972.pdf
↑ ^5.0 ^5.1 https://docs.bbchallenge.org/other/lud20.pdf
↑ https://docs.bbchallenge.org/papers/Brady1983.pdf
↑ https://docs.bbchallenge.org/papers/Dewdney1984.pdf
↑ https://docs.bbchallenge.org/papers/Brady1988.pdf
↑ 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

[:0-1] 1.0 ^1.1 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] 2.0 ^2.1 Determination of the fifth Busy Beaver value. bbchallenge Collaboration et. al. https://arxiv.org/abs/2509.12337

[:1-3] Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52

[:3-4] 4.0 ^4.1 https://docs.bbchallenge.org/papers/Lynn1972.pdf

[:5-5] 5.0 ^5.1 https://docs.bbchallenge.org/other/lud20.pdf

[6] ttps://docs.bbchallenge.org/papers/Brady1983.pdf

[7] ttps://docs.bbchallenge.org/papers/Dewdney1984.pdf

[8] ttps://docs.bbchallenge.org/papers/Brady1988.pdf

[9] Scott Aaronson. 2020. The Busy Beaver Frontier. SIGACT News 51, 3 (August 2020), 32–54. https://doi.org/10.1145/3427361.3427369

[10] ttps://bbchallenge.org/method

[11] ttps://skelet.ludost.net/bb/index.html

[12] 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/

[13] ttps://bbchallenge.org/method#seed-database

[14] Downloadable seed database. https://docs.bbchallenge.org/all_5_states_undecided_machines_with_global_header.zip

[15] ttps://bbchallenge.org/story

[16] ttps://github.com/ccz181078/Coq-BB5

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

@@ 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.
+The BB(5) champion {{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}} and a Σ(5) champion {{TM|1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC|halt}}, were discovered in 1989 by Heiner Marxen and Jürgen Buntrock. These machines were shown to be the definite champions in 2024 by the [[bbchallenge.org]] massively collaborative research project<ref name=":2">Determination of the fifth Busy Beaver value. bbchallenge Collaboration et. al. https://arxiv.org/abs/2509.12337</ref>, proving:
+<math display="block">\begin{array}{lcrl}
+  \operatorname{BB}(5)      & = & 47,176,870 \\
+  \Sigma(5) & = & 4,098 \\
+\end{array}</math>
+BB(5) is the only BB Domain to have [[Irregular Turing Machine|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]].
+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|Busy beaver functions]].
+{| class="wikitable mw-collapsible"
+|+
+! colspan="6" |Timeline of lower bounds established for Σ(5) and S(5)<ref name=":1">Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52 </ref>
+|-
+!Month of discovery
+!Machine
+!S(5) lower bound
+!Σ(5) lower bound
+!Discoverer
+!Notes
+|-
+|?
+|?
+|?
+|≥ 17
+|?
+|Mentioned by Green, M., mentioned by Lynn, D.<ref name=":3">https://docs.bbchallenge.org/papers/Lynn1972.pdf</ref>
+Step count unknown.
+|-
+|November 1964
+|{{TM|1LD1LB_1LZ1LA_0LB1LD_0LE0LD_1RE1RC|halt}}
+|≥ 79
+|(≥ 13)
+|Green, M.
+|Part of an infinite family of machines now known as [[Green's machines]].
+During this period, the steps champion might have been different to the ones champion.
+|-
+| rowspan="2" |August 1972
+|{{TM|1RB1RA_1LC0LD_0RA1LB_1RZ0LE_1RC1RB|halt}}
+|≥ 435
+|(≥ 15)
+| rowspan="2" |Lynn, D.<ref name=":3" />
+| rowspan="2" |During this period, the steps champion was different to the ones champion.
+These bounds were published simultaneously.
+|-
+|{{TM|1RB1RC_1LC1LD_0RA1LB_1RE0LB_1RZ1RD|halt}}
+|(≥ 292)
+|≥ 22
+|-
+| rowspan="2" |November 1973
+|{{TM|1RB0LD_1RC0RB_1LA0RA_0LC0LE_1LC1RZ|halt}}
+|≥ 992
+|(≥ 23)
+| rowspan="2" |Weimann, B.<ref name=":5">https://docs.bbchallenge.org/other/lud20.pdf</ref>
+| rowspan="2" |During this period, the steps champion was different to the ones champion.
+These bounds were published simultaneously.
+|-
+|{{TM|1RB1RA_1RC0RB_1LD1LC_1LE0LC_0RA1RZ|halt}}
+|(≥ 556)
+|≥ 40
+|-
+| rowspan="2" |1974
+|{{TM|0RB1RZ_1RC0LD_1RD0RE_1LB0LD_1RE1RA|halt}}
+|≥ 7,707
+|(≥ 88)
+| rowspan="2" |Lynn, D.<ref>https://docs.bbchallenge.org/papers/Brady1983.pdf</ref>
+| rowspan="2" |During this period, the steps champion was different to the ones champion.
+Bounds were published in 1983.
+These bounds were published simultaneously.
+|-
+|{{TM|1RB0LE_1RC0RA_1LD1RZ_1LE1LD_1LA0LC|halt}}
+|(≥ 6,147)
+|≥ 112
+|-
+|August 1982
+|{{TM|1RB0LC_1RC1RD_1LA0RB_0RE1RZ_1LC1RA|halt}}
+|≥ 134,467
+|≥ 501
+|Schult, U.<ref name=":5" />
+|In 1983, the [https://docs.bbchallenge.org/other/lud20.pdf Dortmund contest] was organised to find new 5-state [[champions]]; Uwe Schult won with this machine.
+|-
+|December 1984
+|{{TM|1RB1LC_0LA0LD_1LA1RZ_1LB1RE_0RD0RB|halt}}
+|≥ 2,133,492
+|≥ 1,915
+| rowspan="2" |Uhing, G.<ref>https://docs.bbchallenge.org/papers/Dewdney1984.pdf</ref><ref>https://docs.bbchallenge.org/papers/Brady1988.pdf</ref>
+|Bound was published by 1985.
+|-
+|February 1986
+|{{TM|1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA|halt}}
+|≥ 2,358,064
+|(≥ 1,471)
+|During this period, the steps champion was different to the ones champion.
+|-
+|August 1989
+|{{TM|1RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC|halt}}
+|≥ 11,798,826
+|≥ 4,098
+| rowspan="3" |Marxen, H., Buntrock, J.<ref name=":0" />
+|Eventually proven to be an Σ(5) champion in 2024.
+|-
+| rowspan="2" |September 1989
+|{{TM|1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB|halt}}
+|≥ 23,554,764
+|(≥ 4,097)
+|During this period, the steps champion was different to the ones champion.
+|-
+|{{TM|1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA|halt}}
+|≥ 47,176,870
+|(≥ 4,098)
+|They did not prove (or claim) that this 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]]).
+Eventually proven to be the S(5) champion and an Σ(5) champion in 2024.
+|}
+=== 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]].<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 deciding the behavior of ~100 million 5-state machines.<ref>https://bbchallenge.org/method</ref>
+* In 2003, Georgi Georgiev (Skelet) published 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 published 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 2021, all BB(5) TMs were enumerated in TNF<ref>https://bbchallenge.org/method#seed-database</ref> and a database of undecided TMs was established.<ref>Downloadable seed database. https://docs.bbchallenge.org/all_5_states_undecided_machines_with_global_header.zip</ref>
+* In 2022, [[bbchallenge.org]] was 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 published [[Coq-BB5]], a Rocq-verified proof of BB(5) = 47,176,870<ref>https://github.com/ccz181078/Coq-BB5</ref>, 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]]):
+* {{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        Σ
+RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA Halt   47176870 4098
+RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt   23554764 4097
+RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ0RB Halt   11821234 4097
+RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ0RB Halt   11821220 4097
+RB1RA_0LC0RC_1RZ1RD_1LE0LA_1LA1LE Halt   11821190 4096
+RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC0LA Halt   11815076 4096
+RB1RA_1LC1LB_1RA0LD_0RB1LE_1RZ1LC Halt   11811040 4097
+RB1RA_1LC1LB_0RC1LD_1RA0LE_1RZ1LC Halt   11811040 4097
+RB1RA_1LC1LB_1RA0LD_1RC1LE_1RZ1LC Halt   11811026 4097
+RB1RA_0LC0RC_1RZ1RD_1LE1RB_1LA1LE Halt   11811010 4096
+RB1RA_1LC1LB_1RA1LD_0RE0LE_1RZ1LC Halt   11804940 4097
+RB1RA_1LC1LB_1RA1LD_1RA0LE_1RZ1LC Halt   11804926 4097
+RB1RA_1LC0RD_1LA1LC_1RZ1RE_0LE1RB Halt   11804910 4096
+RB1RA_1LC0RD_1LA1LC_1RZ1RE_1LC1RB Halt   11804896 4096
+RB1RA_1LC1LB_1RA1LD_1RA1LE_1RZ0LC Halt   11798826 4098
+RB1RA_1LC1RD_1LA1LC_1RZ0RE_1LC1RB Halt   11798796 4097
+RB1RA_1LC1RD_1LA1LC_1RZ1RE_0LE0RB Halt   11792724 4097
+RB1RA_1LC1RD_1LA1LC_1RZ1RE_1LA0RB Halt   11792696 4097
+RB1RA_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt   11792682 4097
+RB1RZ_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
-=== Finding the 5-state winner ===
+== Deciders ==
+All non-halting BB(5) TMs (except for 13 "sporadic" TMs) were decided by the following deciders:
-* 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>
+* [[Cycler]], [[Translated Cycler]]
-* In 1972, Lynn establishes S(5) ≥ 435 and Σ(5) ≥ 22.<ref name=":1" />
+* [[n-Gram CPS]]
-* In 1973, Weimann establishes S(5) ≥ 556 and Σ(5) ≥ 40.<ref name=":1" />
+* [[Repeated Word List (RepWL)]]
-* 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.
+* [[Finite Automata Reduction (FAR)]]
-* 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.
+* [[Weighted Finite Automata Reduction]] (WFAR)
-* 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 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 [[Deciders]].<ref name=":0" />
-=== Proving that the 5-state winner is actually the winner ===
+These 13 sporadic TMs were each decided by individual proofs:
-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 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>
+* [[Skelet 1]]
-* 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>
+* [[Skelet 10]]
-* In 2022, [[bbchallenge.org]] is released, with the aim of collaboratively proving that BB(5) = 47,176,870.<ref>https://bbchallenge.org/story</ref>
+* [[Skelet 17]]
-* 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]].
+* 5 [[Shift overflow counter|Shift overflow counters]] ([[Skelet 15]], [[Skelet 26|26]], [[Skelet 33|33]], 34, 35)
+* 5 Finned Machines (ex: [[Finned 3]])
+See the BB(5) paper<ref name=":2" /> for more details.
+== See also ==
+* [[Skelet 17]]
+* [[BB(6)]]
 == References ==
+<references />
+[[Category:BB Domains]][[Category:BB(5)]]

BB(5): Difference between revisions

Latest revision as of 14:26, 25 September 2026

Contents

History

Proving that the 5-state winner is actually the winner

Champions

Top Halters

Deciders

See also

References

Navigation menu

BB(5): Difference between revisions

Latest revision as of 14:26, 25 September 2026

History

Proving that the 5-state winner is actually the winner

Champions

Top Halters

Deciders

See also

References

Navigation menu

Search