Main Page: Difference between revisions

Latest revision as of 19:48, 10 August 2025

The Busy Beaver function BB (called S originally) was introduced by Tibor Radó in 1962 for 2-symbol Turing machines and later generalised to m-symbol Turing machines:^[1]^[2]

BB(n, m) = Maximum number of steps taken by a halting n-state, m-symbol Turing machine starting from a blank (all 0) tape

The 2-symbol case BB(n, 2) is abbreviated as BB(n). The busy beaver function is not computable, but a few of its values are known:

Small busy beaver values^[3]
	2-state	3-state	4-state	5-state	6-state	7-state
2-symbol	BB(2) = 6	BB(3) = 21	BB(4) = 107	BB(5) = 47,176,870	BB(6) > $2\uparrow \uparrow \uparrow 5$	BB(7) > $2\uparrow ^{11}2\uparrow ^{11}3$
3-symbol	BB(2,3) = 38	BB(3,3) > $10^{17}$	BB(4,3) > $2\uparrow \uparrow \uparrow 2^{2^{32}}$
4-symbol	BB(2,4) = 3,932,964	BB(3,4) > $2\uparrow ^{15}5$
5-symbol	BB(2,5) > $10\uparrow \uparrow 4$	BB(3,5) > $f_{\omega }(2\uparrow ^{15}5)$
6-symbol	BB(2,6) > $10\uparrow \uparrow \uparrow 3$

In the above table, cells are highlighted in orange when there are known Cryptids (mathematically-hard machines) in that class, and cells are highlighted in light orange when the existence of a Cryptid is given by using a known one with less states or symbols.

About bbchallenge

bbchallenge is a massively collaborative research project whose general goal is to obtain more knowledge on the Busy Beaver function. In practice, it mainly consists in collaboratively building Deciders, programs that automatically prove that some Turing machines do not halt. Other efforts also include:

Formalising results using theorem provers (such as Coq)
Maintaining Holdouts lists for small busy beaver values
Proving the behavior of Individual machines
Finding Cryptids (mathematically-hard machines)
Searching for new Champions
Building Accelerated Simulators to simulate halting machines faster
Writing papers and giving talks about busy beaver, see Papers & Talks

In June 2024, bbchallenge achieved a significant milestone by proving in Coq / Rocq that the 5th busy beaver value, BB(5), is equal to the lower bound found in 1989: 47,176,870.^[4]

This Month in Beaver Research (TMBR)

This Month in Beaver Research (TMBR, pronounced "timber") is a monthly summary of Busy Beaver research progress. Here are the three most recent entries:

Contribute to this wiki

This wiki is collaborative, feel free to contribute by editing existing pages or creating new ones:

Notes

↑ Rado, T. (1962), On Non-Computable Functions. Bell System Technical Journal, 41: 877-884. https://doi.org/10.1002/j.1538-7305.1962.tb00480.x
↑ Brady, Allen H, and the Meaning of Life, 'The Busy Beaver Game and the Meaning of Life', in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (Oxford, 1990; online edn, Oxford Academic, 31 Oct. 2023), https://doi.org/10.1093/oso/9780198537748.003.0009, accessed 8 June 2024.
↑ P. Michel, "Historical survey of Busy Beavers".
↑ 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

[1] Rado, T. (1962), On Non-Computable Functions. Bell System Technical Journal, 41: 877-884. https://doi.org/10.1002/j.1538-7305.1962.tb00480.x

[2] Brady, Allen H, and the Meaning of Life, 'The Busy Beaver Game and the Meaning of Life', in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (Oxford, 1990; online edn, Oxford Academic, 31 Oct. 2023), https://doi.org/10.1093/oso/9780198537748.003.0009, accessed 8 June 2024.

[3] P. Michel, "Historical survey of Busy Beavers".

[4] 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

[1]

[2]

[3]

[4]

@@ Line 1: / Line 1: @@
-The [[Busy Beaver function]] BB (called S originally) was introduced by [https://en.wikipedia.org/wiki/Tibor_Rad%C3%B3 Tibor Radó] in 1962 <ref>Rado, T. (1962), On Non-Computable Functions. Bell System Technical Journal, 41: 877-884. https://doi.org/10.1002/j.1538-7305.1962.tb00480.x</ref> for 2-symbol [[Turing machines]] and later generalised<ref>Brady, Allen H, and the Meaning of Life, 'The Busy Beaver Game and the Meaning of Life', in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (Oxford, 1990; online edn, Oxford Academic, 31 Oct. 2023), https://doi.org/10.1093/oso/9780198537748.003.0009, accessed 8 June 2024.</ref> to m-symbol Turing machines:
+The [[Busy Beaver function]] BB (called ''S'' originally) was introduced by [https://en.wikipedia.org/wiki/Tibor_Rad%C3%B3 Tibor Radó] in 1962 for 2-symbol [[Turing machines]] and later generalised to ''m''-symbol Turing machines:<ref>Rado, T. (1962), On Non-Computable Functions. Bell System Technical Journal, 41: 877-884. https://doi.org/10.1002/j.1538-7305.1962.tb00480.x</ref><ref>Brady, Allen H, and the Meaning of Life, 'The Busy Beaver Game and the Meaning of Life', in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (Oxford, 1990; online edn, Oxford Academic, 31 Oct. 2023), https://doi.org/10.1093/oso/9780198537748.003.0009, accessed 8 June 2024.</ref>
 {| class="wikitable"
 |-
-| BB(n,m) = Maximum number of steps done by a halting m-symbol Turing machine with n states starting from all-0 memory tape
+| BB(''n'', ''m'') = Maximum number of steps taken by a halting ''n''-state, ''m''-symbol Turing machine starting from a blank (all 0) tape
 |}
-The busy beaver function is not computable and, few of its values are known:
+The 2-symbol case BB(''n'', 2) is abbreviated as BB(''n''). The busy beaver function is not computable, but a few of its values are known:
 {| class="wikitable"
-|+ Small busy beaver values <ref>https://bbchallenge.org/~pascal.michel/ha.html</ref>  <ref name=":0">https://bbchallenge.org/</ref>
+|+ Small busy beaver values<ref>P. Michel, "[https://bbchallenge.org/~pascal.michel/ha.html Historical survey of Busy Beavers]".</ref>
-|-
+! !!2-state!!3-state !!4-state!!5-state!!6-state
-|   || 2-state || 3-state || 4-state || 5-state || 6-state || 7-state
+!7-state
 |-
-| 2-symbol
+! 2-symbol
 | [[BB(2)]] = 6
 | [[BB(3)]] = 21
 | [[BB(4)]] = 107
 | [[BB(5)]] = 47,176,870
-| [[BB(6)]] > <math>10 \uparrow \uparrow 15</math>
+| style="background: orange;" | [[BB(6)]] > <math>2 \uparrow \uparrow \uparrow 5</math>
-| style="background: orange;" | [[BB(7)]]
+| style="background: orange;" | [[BB(7)]] > <math>2 \uparrow^{11} 2 \uparrow^{11} 3</math>
 |-
-| 3-symbol  || [[BB(2,3)]] = 38
+! 3-symbol
+| [[BB(2,3)]] = 38
 | style="background: orange;" | [[BB(3,3)]] > <math>10^{17}</math>
-| style="background: #ffe4b2;" | [[BB(4,3)]] > <math>10^{14072}</math>
+| style="background: #ffe4b2;" | [[BB(4,3)]] > <math>2 \uparrow\uparrow\uparrow 2^{2^{32}}</math>
 | style="background: #ffe4b2;" |
 | style="background: #ffe4b2;" |
 | style="background: #ffe4b2;" |
 |-
-| 4-symbol
+! 4-symbol
 | [[BB(2,4)]] = 3,932,964
-| style="background: #ffe4b2;" | [[BB(3,4)]] ≥ <math>2 \uparrow^{15} 5 + 14</math>
+| style="background: #ffe4b2;" | [[BB(3,4)]] > <math>2 \uparrow^{15} 5</math>
 | style="background: #ffe4b2;" |
 | style="background: #ffe4b2;" |
@@ Line 36: / Line 37: @@
 | style="background: #ffe4b2;" |
 |-
-| 5-symbol
+! 5-symbol
-| style="background: orange;" | [[BB(2,5)]] > 6.5 × <math>10^{38033}</math>
+| style="background: orange;" | [[BB(2,5)]] > <math>10\uparrow\uparrow 4</math>
+| style="background: #ffe4b2;" | [[BB(3,5)]] > <math> f_\omega(2 \uparrow^{15} 5)</math>
+| style="background: #ffe4b2;" |
+| style="background: #ffe4b2;" |
+| style="background: #ffe4b2;" |
+| style="background: #ffe4b2;" |
+|-
+! 6-symbol
+| style="background: #ffe4b2;" | [[BB(2,6)]] > <math>10 \uparrow\uparrow\uparrow 3</math>
 | style="background: #ffe4b2;" |
 | style="background: #ffe4b2;" |
@@ Line 43: / Line 52: @@
 | style="background: #ffe4b2;" |
 | style="background: #ffe4b2;" |
 |}
-In the above table, <span style="background: orange">cells are highlighted in orange</span> when there are known [[Cryptids]] (mathematically-hard machines) in that class.
+In the above table, <span style="background: orange">cells are highlighted in orange</span> when there are known [[Cryptids]] (mathematically-hard machines) in that class, and <span style="background: #ffe4b2">cells are highlighted in light orange</span> when the existence of a Cryptid is given by using a known one with less states or symbols.
-== bbchallenge.org ==
+== About bbchallenge ==
-[[bbchallenge.org]] <ref name=":0" /> is a massively collaborative research project whose general goal is to obtain more knowledge on the [[Busy Beaver function]]. In practice, it mainly consists in collaboratively building [[Deciders]], programs that automatically prove that some Turing machines do not halt.  Other efforts also include:
+[https://www.bbchallenge.org bbchallenge] is a massively collaborative research project whose general goal is to obtain more knowledge on the [[Busy Beaver function]]. In practice, it mainly consists in collaboratively building [[Deciders]], programs that automatically prove that some Turing machines do not halt.  Other efforts also include:
 * Formalising results using theorem provers (such as [https://en.wikipedia.org/wiki/Coq_(software) Coq])
@@ Line 55: / Line 63: @@
 * Proving the behavior of [[:Category:Individual Machines|Individual machines]]
 * Finding [[Cryptids]] (mathematically-hard machines)
+* Searching for new [[Champions]]
 * Building [[Accelerated Simulator]]s to simulate halting machines faster
+* Writing papers and giving talks about busy beaver, see [[Papers & Talks]]
+In June 2024, bbchallenge achieved a significant milestone by proving in Coq / Rocq that the 5th busy beaver value, [[BB(5)]], is equal to the lower bound found in 1989: 47,176,870.<ref>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>
+== This Month in Beaver Research (TMBR) ==
+[[:Category:This Month in Beaver Research|This Month in Beaver Research]] (TMBR, pronounced "timber") is a monthly summary of Busy Beaver research progress. Here are the three most recent entries:
-Notably, as part of bbchallenge.org, in June 2024 the 5th busy beaver value [[BB(5)]] was proven in Coq to be equal to the lower bound found in 1989<ref>H. Marxen and J. Buntrock. Attacking the Busy Beaver 5.
+* [[TMBR: August 2025|TMBR August 2025]]
-Bulletin of the EATCS, 40, pages 247-251, February 1990. https://turbotm.de/~heiner/BB/mabu90.html</ref>: 47,176,870.
+* [[TMBR: July 2025|TMBR July 2025]]
 == Contribute to this wiki ==