BB(5): Difference between revisions

Revision as of 13:27, 19 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]

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.


Timeline of lower bounds established for Σ(5) and S(5)^[3]^[4]
Month of discovery	Machine	S(5) lower bound	Σ(5) lower bound	Discoverer	Notes
?	?	?	≥ 17	?	Mentioned by Green, M., mentioned by Brady, A.^[5] Step count unknown.
November 1964	`1RD1RB_1RZ1RA_0RB1RD_0RE0RD_1LE1LC` (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.	During this period, the steps champion was different to the ones champion.
August 1972	`1RB1RC_1LC1LD_0RA1LB_1RE0LB_1RZ1RD` (bbch)	(≥ 292)	≥ 22	Lynn, D.
October 1973		≥ 556	≥ 40	Weimann, B.	TODO: Find machine in ^[6], because the editor can't read German.
1974	`1RB0LC_1RC0RD_1LA0LC_1RD1RE_0RA1RZ` (bbch)	≥ 7,706	(≥ 88)	Lynn, D.	Lynn's stopping convention for these machines seems to return a stopping value one greater than the modern stopping convention. During this period, the steps champion was different to the ones champion. Bounds were only published in 1983.
1974	`1RB0LE_1RC0RA_1LD1RZ_1LE1LD_1LA0LC` (bbch)	(≥ 6,147)	≥ 112	Lynn, D.
August 1982	`1RB0LC_1RC1RD_1LA0RB_0RE1RZ_1LC1RA` (bbch)	≥ 134,467	≥ 501	Schult, U,	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.
February 1986	`1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA` (bbch)	≥ 2,358,064	(≥ 1,471)	Uhing, G.	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.	Eventually proven to be one of the Σ(5) champions 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).^[1] Eventually proven to be the S(5) champion and one of the Σ(5) champions 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.^[7] In practice, proving this conjecture requires deciding the behavior of ~100 million 5-state machines.^[8]

In 2003, Georgi Georgiev (Skelet) published a list of 43 holdouts, based on bbfind, a collection of Deciders written in Pascal.^[9]
In 2009, Joachim Hertel published a method claiming 100 holdouts.^[10]
In 2021, all BB(5) TMs were enumerated in TNF^[11] and a database of undecided TMs was established.^[12]
In 2022, bbchallenge.org was released, with the aim of collaboratively proving that BB(5) = 47,176,870.^[13]
In 2024, bbchallenge's contributor @mxdys published Coq-BB5, a Rocq-verified proof of BB(5) = 47,176,870^[14], 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. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62
↑ Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52
↑ https://docs.bbchallenge.org/papers/Brady1965.pdf
↑ https://docs.bbchallenge.org/papers/WeimannCasperFenzl1973.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

[:PMH-3] Pascal Michel. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62

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

[5] ttps://docs.bbchallenge.org/papers/Brady1965.pdf

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

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

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

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

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

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

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

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

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

@@ Line 7: / Line 7: @@
 == 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]].
+{| class="wikitable"
-=== Finding the 5-state winner ===
+|+
+! colspan="6" |Timeline of lower bounds established for Σ(5) and S(5)<ref name=":PMH">Pascal Michel. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62</ref><ref name=":1">Pascal Michel. (2022). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm52 </ref>
-* In 1964, Green established Σ(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 established S(5) ≥ 435 and Σ(5) ≥ 22.<ref name=":1" />
+!Month of discovery
-* In 1973, Weimann established S(5) ≥ 556 and Σ(5) ≥ 40.<ref name=":1" />
+!Machine
-* 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>, established S(5) ≥ 7,707 and Σ(5) ≥ 112.
+!S(5) lower bound
-* In 1983, the [https://docs.bbchallenge.org/other/lud20.pdf Dortmund contest] was organised to find new 5-state [[champions]]. The winner was Uwe Schult, who established S(5) ≥ 134,467 and Σ(5) ≥ 501.
+!Σ(5) lower bound
-* In 1984, George Uhing established S(5) ≥ 2,133,492 and Σ(5) ≥ 1,915.<ref>https://docs.bbchallenge.org/other/busy.html</ref>
+!Discoverer
-* In 1989, Heiner Marxen and Jürgen Buntrock found a [[5-state busy beaver winner|new champion]], establishing S(5) ≥ 47,176,870 and Σ(5) ≥ 4,098.<ref name=":0" /> 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]]).<ref name=":0" />
+!Notes
+|-
+|?
+|?
+|?
+|≥ 17
+|?
+|Mentioned by Green, M., mentioned by Brady, A.<ref>https://docs.bbchallenge.org/papers/Brady1965.pdf</ref>
+Step count unknown.
+|-
+|November 1964
+|{{TM|1RD1RB_1RZ1RA_0RB1RD_0RE0RD_1LE1LC|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.
+| rowspan="2" |During this period, the steps champion was different to the ones champion.
+|-
+|{{TM|1RB1RC_1LC1LD_0RA1LB_1RE0LB_1RZ1RD|halt}}
+|(≥ 292)
+|≥ 22
+|-
+|October 1973
+|
+|≥ 556
+|≥ 40
+|Weimann, B.
+|TODO: Find machine in <ref>https://docs.bbchallenge.org/papers/WeimannCasperFenzl1973.pdf</ref>, because the editor can't read German.
+|-
+| rowspan="2" |1974
+|{{TM|1RB0LC_1RC0RD_1LA0LC_1RD1RE_0RA1RZ|halt}}
+|≥ 7,706
+|(≥ 88)
+| rowspan="2" |Lynn, D.
+| rowspan="2" |Lynn's stopping convention for these machines seems to return a stopping value one greater than the modern stopping convention.
+During this period, the steps champion was different to the ones champion.
+Bounds were only published in 1983.
+|-
+|{{TM|1RB0LE_1RC0RA_1LD1RZ_1LE1LD_1LA0LC|halt}}
+|(≥ 6,147)
+|≥ 112
+|-
+|August 1982
+|{{TM|1RB0LC_1RC1RD_1LA0RB_0RE1RZ_1LC1RA|halt}}
+|≥ 134,467
+|≥ 501
+|Schult, U,
+|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.
+|
+|-
+|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.
+|Eventually proven to be one of the Σ(5) champions 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]]).<ref name=":0" />
+Eventually proven to be the S(5) champion and one of the Σ(5) champions in 2024.
+|}
 === Proving that the 5-state winner is actually the winner ===
@@ Line 38: / Line 125: @@
 == Top Halters ==
 The top 20 longest running BB(5) TMs (in [[TNF-1RB]]) are:
-<pre>
+<pre>Standard format                    Status S        Σ
-Standard format                    Status S        Σ
 RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA Halt   47176870 4098
 RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt   23554764 4097
@@ Line 59: / Line 145: @@
 RB1RA_1LC1RD_1LA1LC_1RZ1RE_1LA0RB Halt   11792696 4097
 RB1RA_1LC1RD_1LA1LC_1RZ1RE_1RA0RB Halt   11792682 4097
-RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA Halt   2358064  1471
+RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA Halt   2358064  1471</pre>
-</pre>
 For more top halting BB(5) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/5x2

BB(5): Difference between revisions

Revision as of 13:27, 19 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

Revision as of 13:27, 19 September 2026

History

Proving that the 5-state winner is actually the winner

Champions

Top Halters

Deciders

See also

References

Navigation menu

Search