BB(5): Difference between revisions
Jump to navigation
Jump to search
actually this is a better way of stating it |
conflict |
||
| (One intermediate revision by the same user not shown) | |||
| Line 50: | Line 50: | ||
| style="background: #FFCCCC;" |≥ 13 | | style="background: #FFCCCC;" |≥ 13 | ||
|Lee, C. Y<ref>https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486567232687544</ref> | |Lee, C. Y<ref>https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486567232687544</ref> | ||
|Eventually proven (informally) to be a Σ(4) champion in | |Eventually proven (informally) to be a Σ(4) champion in 1983. | ||
|- | |- | ||
|October 1966 | |October 1966 | ||
| Line 57: | Line 57: | ||
| style="background: #FFCCCC;" |≥ 13 | | style="background: #FFCCCC;" |≥ 13 | ||
|Brady, A.<ref name=":12">Brady, A. H. (1966). The Conjectured Highest Scoring Machines for Rado's Σ(k) for the Value k = 4. https://ieeexplore.ieee.org/document/4038890</ref> | |Brady, A.<ref name=":12">Brady, A. H. (1966). The Conjectured Highest Scoring Machines for Rado's Σ(k) for the Value k = 4. https://ieeexplore.ieee.org/document/4038890</ref> | ||
|Eventually proven (informally) to be the S(4) and a Σ(4) champion in | |Eventually proven (informally) to be the S(4) and a Σ(4) champion in 1983. | ||
|- | |- | ||
| rowspan="2" |August 1972 | | rowspan="2" |August 1972 | ||
| Line 74: | Line 74: | ||
|≥ 992 | |≥ 992 | ||
| style="background: #FFCCCC;" |≥ 23 | | style="background: #FFCCCC;" |≥ 23 | ||
| rowspan="2" |Weimann, B.<ref name=":5">https://docs.bbchallenge.org/other/lud20.pdf</ref> | | rowspan="2" |Weimann, B.<ref name=":5">https://docs.bbchallenge.org/other/lud20.pdf</ref> | ||
| rowspan="2" |These bounds were published simultaneously. | | rowspan="2" |These bounds were published simultaneously. | ||
|- | |- | ||
| Line 117: | Line 117: | ||
|≥ 11,798,826 | |≥ 11,798,826 | ||
|≥ 4,098 | |≥ 4,098 | ||
| rowspan="3" |Marxen, H., Buntrock, J.<ref name=":0" /> | | rowspan="3" |Marxen, H., Buntrock, J.<ref name=":0" /> | ||
|Eventually proven to be an Σ(5) champion in 2024. | |Eventually proven to be an Σ(5) champion in 2024. | ||
|- | |- | ||
| rowspan="2" |September 1989 | | rowspan="2" |September 1989 | ||
|{{TM|1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB|halt}} | |{{TM|1RB0LD_1LC1RD_1LA1LC_1RZ1RE_1RA0RB|halt}} | ||
|≥ 23,554,764 | |≥ 23,554,764 | ||
| Line 133: | Line 133: | ||
|- | |- | ||
|June 2024 | |June 2024 | ||
|'''= 47,176,870''' | |'''= 47,176,870''' | ||
|'''= 4,098''' | |'''= 4,098''' | ||
|bbchallenge<ref name=":4" /> | |bbchallenge<ref name=":4" /> | ||
|The bbchallenge proved S(5) = 47,176,870 and Σ(5) = 4,098 using [[Coq-BB5]]. | |The bbchallenge proved S(5) = 47,176,870 and Σ(5) = 4,098 using [[Coq-BB5]]. | ||
| Line 146: | Line 146: | ||
* 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 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 2022, [[bbchallenge.org]] was released, with the aim of collaboratively proving that BB(5) = 47,176,870.<ref>https://bbchallenge.org/story</ref> | ||
* In | |||
* In 2024, bbchallenge's contributor @mxdys published [[Coq-BB5]], a Rocq-verified proof of BB(5) = 47,176,870<ref name=":4">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. | * In 2024, bbchallenge's contributor @mxdys published [[Coq-BB5]], a Rocq-verified proof of BB(5) = 47,176,870<ref name=":4">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. | ||
Latest revision as of 17:17, 8 October 2026
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]
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:
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 bounds established for Σ(5) and S(5)[3] | |||||
|---|---|---|---|---|---|
| Month of discovery | Machine | S(5) | Σ(5) | Discoverer | Notes |
| ? | ? | ? | ≥ 17 | ? | Mentioned by Green, M., mentioned by Lynn, D.[4]
Green, M. did not include the machine which demonstated this bound. |
| 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. |
| December 1964 | 1RB1LD_0LC0RC_1LC1LA_1RZ0LA (bbch)
|
≥ 84 | ≥ 11 | Brady, A.[5] | |
| 1965 | 1RB0RC_1LA1RA_1RZ1RD_1LD0LB (bbch)
|
≥ 96 | ≥ 13 | Lee, C. Y[6] | Eventually proven (informally) to be a Σ(4) champion in 1983. |
| October 1966 | 1RB1LB_1LA0LC_1RZ1LD_1RD0RA (bbch)
|
≥ 107 | ≥ 13 | Brady, A.[7] | Eventually proven (informally) to be the S(4) and a Σ(4) champion in 1983. |
| August 1972 | 1RB1RA_1LC0LD_0RA1LB_1RZ0LE_1RC1RB (bbch)
|
≥ 435 | ≥ 15 | Lynn, D.[4] | These bounds were published simultaneously. |
1RB1RC_1LC1LD_0RA1LB_1RE0LB_1RZ1RD (bbch)
|
≥ 292 | ≥ 22 | |||
| November 1973 | 1RB0LD_1RC0RB_1LA0RA_0LC0LE_1LC1RZ (bbch)
|
≥ 992 | ≥ 23 | Weimann, B.[8] | These bounds were published simultaneously. |
1RB1RA_1RC0RB_1LD1LC_1LE0LC_0RA1RZ (bbch)
|
≥ 556 | ≥ 40 | |||
| 1974 | 0RB1RZ_1RC0LD_1RD0RE_1LB0LD_1RE1RA (bbch)
|
≥ 7,707 | ≥ 88 | Lynn, D.[9] | These bounds were published simultaneously in April 1983. |
1RB0LE_1RC0RA_1LD1RZ_1LE1LD_1LA0LC (bbch)
|
≥ 6,147 | ≥ 112 | |||
| August 1982 | 1RB0LC_1RC1RD_1LA0RB_0RE1RZ_1LC1RA (bbch)
|
≥ 134,467 | ≥ 501 | Schult, U.[8] | In 1983, the Dortmund contest was organised to find new 5-state champions; Uwe Schult won with this machine.
Bound was published in January 1983. |
| December 1984 | 1RB1LC_0LA0LD_1LA1RZ_1LB1RE_0RD0RB (bbch)
|
≥ 2,133,492 | ≥ 1,915 | Uhing, G.[10][11] | Bound was published by 1985. |
| February 1986 | 1RB1RZ_1LC1RC_0RE0LD_1LC0LB_1RD1RA (bbch)
|
≥ 2,358,064 | ≥ 1,471 | ||
| 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 | ||
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. | ||
| June 2024 | = 47,176,870 | = 4,098 | bbchallenge[12] | The bbchallenge proved S(5) = 47,176,870 and Σ(5) = 4,098 using Coq-BB5. | |
Bounds highlighted in red indicate those which did not improve upon the best known at the time. Machines highlighted in blue were inherited from the hunt for BB(4).
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.[13] In practice, proving this conjecture requires deciding the behavior of ~100 million 5-state machines.[14]
- In 2003, Georgi Georgiev (Skelet) published a list of 43 holdouts, based on bbfind, a collection of Deciders written in Pascal.[15]
- In 2009, Joachim Hertel published a method claiming 100 holdouts.[16]
- In 2021, all BB(5) TMs were enumerated in TNF[17] and a database of undecided TMs was established.[18]
- In 2022, bbchallenge.org was released, with the aim of collaboratively proving that BB(5) = 47,176,870.[19]
- In
- In 2024, bbchallenge's contributor @mxdys published Coq-BB5, a Rocq-verified proof of BB(5) = 47,176,870[12], 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 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
- ↑ Brady, A. H. (1965). Solutions of restricted cases of the halting problem applied to the determination of particular values of a non-computable function. https://ir.library.oregonstate.edu/concern/graduate_thesis_or_dissertations/zk51vk21c
- ↑ https://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486567232687544
- ↑ Brady, A. H. (1966). The Conjectured Highest Scoring Machines for Rado's Σ(k) for the Value k = 4. https://ieeexplore.ieee.org/document/4038890
- ↑ 8.0 8.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
- ↑ 12.0 12.1 https://github.com/ccz181078/Coq-BB5
- ↑ 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