BB(4): Difference between revisions

Latest revision as of 15:46, 25 September 2026

The 4-state, 2-symbol Busy Beaver problem, BB(4), refers to the 4^th value of the Busy Beaver function. In 1983, the 4-state busy beaver winner was found: a 4-state Turing machine halting after 107 steps giving the lower bound BB(4) ≥ 107.

In 2024, BB(4) = 107 was officially confirmed by the bbchallenge.org massively collaborative research project, when a proof for the BB(4) case was added to Coq-BB5 and successfully compiled.^[1]

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 Σ(4) and S(4)
Month of discovery	Machine	S(4) lower bound	Σ(4) lower bound	Discoverer	Notes
?	?	?	≥ 12	?	Mentioned by Green, M. in November 1964. Due to exhaustive simulations, it is known that the result S(4) ≥ 53 could have been stated at the time, but was not.
December 1964	`1RB1LD_0LC0RC_1LC1LA_1RZ0LA` (bbch)	≥ 84	(≥ 11)	Brady, A.^[2]	The bound for the ones champion was equalled by an earlier, unknown machine. These bounds were published simultaneously.
December 1964	`1RB0LA_1RC1LB_1LB1RD_1RZ0RA` (bbch)	(≥ 63)	(≥ 12)	Brady, A.^[2]
1965	`1RB0RC_1LA1RA_1RZ1RD_1LD0LB` (bbch)	≥ 96	≥ 13	Lee, C. Y^[3]	Eventually proven (informally) to be a Σ(4) champion in 1974.
October 1966	`1RB1LB_1LA0LC_1RZ1LD_1RD0RA` (bbch)	≥ 107	(≥ 13)	Brady, A.^[4]	Eventually proven (informally) to be the S(4) and a Σ(4) champion in 1974.

In 1966, Allen Brady conjectured Σ(4) = 13 and S(4) = 107 (Brady stated S(4) = 106, seemingly basing it upon a slightly different version of S function).^[4]
In 1974, Allen Brady proved that S(4) = 107.^[5]
In 1983, Allen Brady published the proof that Σ(4) = 13 and S(4) = 107. ^[6] Some holdouts were not rigorously handled by the proof: "All of the remaining holdouts were examined by means of voluminous printouts of their histories along with some program extracted features. It was determined to the author's satisfaction that none of these machines will ever stop."
In 2024, bbchallenge.org formalized a proof of the bounds Σ(4) = 13 and S(4) = 107 in Rocq, confirming (TODO: state what was confirmed naturally)

Champions

S(4) = 107 and there is only one shift champion (in TNF):

1RB1LB_1LA0LC_1RZ1LD_1RD0RA (bbch) leaves 13 ones (a ones champion)

Σ(4) = 13 and there are 2 ones champions (in TNF):

1RB1LB_1LA0LC_1RZ1LD_1RD0RA (bbch) runs for 107 steps (the steps champion)

1RB0RC_1LA1RA_1RZ1RD_1LD0LB (bbch) runs for 96 steps

Top Halters

In TNF-1RB there are exactly 620,261 BB(4) TMs of which 183,983 halt. The top 20 longest running TMs are:

Standard Format             Status Steps   Σ
1RB1LB_1LA0LC_1RZ1LD_1RD0RA Halt   107     13
1RB1LD_1LC0RB_1RA1LA_1RZ0LC Halt   97      9
1RB0RC_1LA1RA_1RZ1RD_1LD0LB Halt   96      13
1RB1LB_0LC0RD_1RZ1LA_1RA0LA Halt   96      6
1RB1LD_0LC0RC_1LC1LA_1RZ0LA Halt   84      11
1RB1RZ_1LC0RD_1LA1LB_0LC1RD Halt   83      8
1RB0RD_1LC0LA_1RA1LB_1RZ0RC Halt   78      12
1RB1LA_0RC0RD_1LC0LA_1RZ0RC Halt   78      9
1RB0RD_0RC0RA_1LC0LA_0RB1RZ Halt   75      9
1RB0RC_1LC1RA_1RZ0LD_1RA1LA Halt   74      8
1RB1LA_0LA1RC_1RA0RD_1RZ0RB Halt   70      8
1RB1LC_0RC0RB_0LD0LA_1LA1RZ Halt   69      7
1RB1LA_1LA1RC_1RZ0RD_0LD1RB Halt   69      7
1RB1RZ_1LC1RA_0RC0LD_1RD0LB Halt   68      10
1RB0LB_0RC0RD_1LD1LA_0LA1RZ Halt   68      8
1RB1LB_0RC1RZ_1LC1LD_0RD0LA Halt   68      7
1RB0RD_0RC1RZ_1LC0LA_0RA0RB Halt   68      7
1RB0LD_0RC1LD_1LC0RB_0LA1RZ Halt   67      7
1RB1LA_1RC0LD_0LA0RC_1RZ1LB Halt   66      7
1RB1RC_1LC1RD_1RZ0LD_1LA0RA Halt   65      7

For the top 1000 halting BB(4) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/4x2.txt

References

↑ https://github.com/ccz181078/Coq-BB5/blob/main/BB42Theorem.v
↑ 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
↑ ^4.0 ^4.1 Brady, A. H. (1966). The Conjectured Highest Scoring Machines for Rado's Σ(k) for the Value k = 4. https://ieeexplore.ieee.org/document/4038890
↑ https://www.ams.org/journals/notices/197501/197501FullIssue.pdf
↑ Brady, A. H. (1983). The determination of the value of Rado’s noncomputable function Σ(k) for four-state Turing machines. https://www.ams.org/journals/mcom/1983-40-162/S0025-5718-1983-0689479-6/

[1] ttps://github.com/ccz181078/Coq-BB5/blob/main/BB42Theorem.v

[:0-2] 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

[3] ttps://etd.ohiolink.edu/acprod/odb_etd/etd/r/1501/10?clear=10&p10_accession_num=osu1486567232687544

[:1-4] 4.0 ^4.1 Brady, A. H. (1966). The Conjectured Highest Scoring Machines for Rado's Σ(k) for the Value k = 4. https://ieeexplore.ieee.org/document/4038890

[:2-5] ttps://www.ams.org/journals/notices/197501/197501FullIssue.pdf

[:3-6] Brady, A. H. (1983). The determination of the value of Rado’s noncomputable function Σ(k) for four-state Turing machines. https://www.ams.org/journals/mcom/1983-40-162/S0025-5718-1983-0689479-6/

[1]

[2]

[3]

[4]

[5]

[6]

@@ Line 1: / Line 1: @@
-'''BB(4)''' refers to the 4<sup>th</sup> value of the [[Busy Beaver function]].
+The 4-state, 2-symbol Busy Beaver problem, '''BB(4)''', refers to the 4<sup>th</sup> value of the [[Busy Beaver function]]. In 1983, the 4-state busy beaver winner was found: a 4-state [[Turing machine]] halting after 107 steps giving the lower bound BB(4) ≥ 107.
+In 2024, BB(4) = 107 was officially confirmed by the [[bbchallenge.org]] massively collaborative research project, when a proof for the BB(4) case was added to [[Coq-BB5]] and successfully compiled.<ref>https://github.com/ccz181078/Coq-BB5/blob/main/BB42Theorem.v</ref>
 == 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]].
+{| class="wikitable mw-collapsible"
+! colspan="6" |Timeline of lower bounds established for Σ(4) and S(4)
+|-
+!Month of discovery
+!Machine
+!S(4) lower bound
+!Σ(4) lower bound
+!Discoverer
+!Notes
+|-
+|?
+|?
+|?
+|≥ 12
+|?
+|Mentioned by Green, M. in November 1964.
+Due to exhaustive simulations, it is known that the result S(4) ≥ 53 could have been stated at the time, but was not.
+|-
+| rowspan="2" |December 1964
+|{{TM|1RB1LD_0LC0RC_1LC1LA_1RZ0LA|halt}}
+|≥ 84
+|(≥ 11)
+| rowspan="2" |Brady, A.<ref name=":0">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</ref>
+| rowspan="2" |The bound for the ones champion was equalled by an earlier, unknown machine.
+These bounds were published simultaneously.
+|-
+|{{TM|1RB0LA_1RC1LB_1LB1RD_1RZ0RA|halt}}
+|(≥ 63)
+|(≥ 12)
+|-
+|1965
+|{{TM|1RB0RC_1LA1RA_1RZ1RD_1LD0LB|halt}}
+|≥ 96
+|≥ 13
+|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 1974.
+|-
+|October 1966
+|{{TM|1RB1LB_1LA0LC_1RZ1LD_1RD0RA|halt}}
+|≥ 107
+|(≥ 13)
+|Brady, A.<ref name=":1" />
+|Eventually proven (informally) to be the S(4) and a Σ(4) champion in 1974.
+|}
+* In 1966, Allen Brady conjectured Σ(4) = 13 and S(4) = 107 (Brady stated S(4) = 106, seemingly basing it upon a slightly different version of S function).<ref name=":1">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>
+* In 1974, Allen Brady proved that S(4) = 107.<ref name=":2">https://www.ams.org/journals/notices/197501/197501FullIssue.pdf</ref>
+* In 1983, Allen Brady published the proof that Σ(4) = 13 and S(4) = 107. <ref name=":3">Brady, A. H. (1983). The determination of the value of Rado’s noncomputable function Σ(k) for four-state Turing machines. https://www.ams.org/journals/mcom/1983-40-162/S0025-5718-1983-0689479-6/</ref>  Some holdouts were not rigorously handled by the proof:  ''"All of the remaining holdouts were examined by means of voluminous printouts of their histories along with some program extracted features. It was determined to the author's satisfaction that none of these machines will ever stop."''
+* In 2024, [[bbchallenge.org]] formalized a proof of the bounds Σ(4) = 13 and S(4) = 107 in Rocq, confirming (TODO: state what was confirmed naturally)
+== Champions ==
+S(4) = 107 and there is only one shift [[champion]] (in [[TNF]]):
+* {{TM|1RB1LB_1LA0LC_1RZ1LD_1RD0RA|halt}} leaves 13 ones (a ones champion)
+Σ(4) = 13 and there are 2 ones champions (in TNF):
+* {{TM|1RB1LB_1LA0LC_1RZ1LD_1RD0RA|halt}} runs for 107 steps (the steps champion)
-* In 1965, Allen Brady proves that S(4) ≥ 84 and Σ(4) ≥ 11.<ref name=":0">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</ref> (TODO: the abstract says "or ≥ 12 using a different stopping convention")
+* {{TM|1RB0RC_1LA1RA_1RZ1RD_1LD0LB|halt}} runs for 96 steps
-* In 1966, Allen Brady conjectures Σ(4) = 13 and S(4) = 107 (He says S(4) = 106, but this seems to be based upon a slightly different version of S function).<ref name=":1">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>
-* In 1974, Allen Brady proves that S(4) = 107.<ref name=":2">https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/</ref> (better source needed)
-* In 1983, Allen Brady publishes the proof that Σ(4) = 13 and S(4) = 107. <ref name=":3">Brady, A. H. (1983). The determination of the value of Rado’s noncomputable function Σ(k) for four-state Turing machines. https://www.ams.org/journals/mcom/1983-40-162/S0025-5718-1983-0689479-6/</ref>
+== Top Halters ==
+In [[TNF-1RB]] there are exactly 620,261 BB(4) TMs of which 183,983 halt. The top 20 longest running TMs are:
+<pre>
+Standard Format             Status Steps   Σ
+RB1LB_1LA0LC_1RZ1LD_1RD0RA Halt   107     13
+RB1LD_1LC0RB_1RA1LA_1RZ0LC Halt   97      9
+RB0RC_1LA1RA_1RZ1RD_1LD0LB Halt   96      13
+RB1LB_0LC0RD_1RZ1LA_1RA0LA Halt   96      6
+RB1LD_0LC0RC_1LC1LA_1RZ0LA Halt   84      11
+RB1RZ_1LC0RD_1LA1LB_0LC1RD Halt   83      8
+RB0RD_1LC0LA_1RA1LB_1RZ0RC Halt   78      12
+RB1LA_0RC0RD_1LC0LA_1RZ0RC Halt   78      9
+RB0RD_0RC0RA_1LC0LA_0RB1RZ Halt   75      9
+RB0RC_1LC1RA_1RZ0LD_1RA1LA Halt   74      8
+RB1LA_0LA1RC_1RA0RD_1RZ0RB Halt   70      8
+RB1LC_0RC0RB_0LD0LA_1LA1RZ Halt   69      7
+RB1LA_1LA1RC_1RZ0RD_0LD1RB Halt   69      7
+RB1RZ_1LC1RA_0RC0LD_1RD0LB Halt   68      10
+RB0LB_0RC0RD_1LD1LA_0LA1RZ Halt   68      8
+RB1LB_0RC1RZ_1LC1LD_0RD0LA Halt   68      7
+RB0RD_0RC1RZ_1LC0LA_0RA0RB Halt   68      7
+RB0LD_0RC1LD_1LC0RB_0LA1RZ Halt   67      7
+RB1LA_1RC0LD_0LA0RC_1RZ1LB Halt   66      7
+RB1RC_1LC1RD_1RZ0LD_1LA0RA Halt   65      7
+</pre>
+For the top 1000 halting BB(4) TMs, see: https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/4x2.txt
 == References ==
+<references />
+[[Category:BB Domains]]
+[[Category:BB(4)]]

BB(4): Difference between revisions

Latest revision as of 15:46, 25 September 2026

Contents

History

Champions

Top Halters

References

Navigation menu

BB(4): Difference between revisions

Latest revision as of 15:46, 25 September 2026

History

Champions

Top Halters

References

Navigation menu

Search