BB(4): Difference between revisions
Jump to navigation
Jump to search
No edit summary |
No edit summary |
||
| Line 7: | Line 7: | ||
* 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 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 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> | * 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> 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."''<ref name=":0" /> | ||
* In 2024, S(4) = 107 was confirmed as part of [[Coq-BB5]]. <ref>https://github.com/ccz181078/Coq-BB5/blob/main/BB42Theorem.v</ref> | |||
== References == | == References == | ||
Revision as of 15:19, 11 July 2024
BB(4) refers to the 4th value of the Busy Beaver function.
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 1965, Allen Brady proves that S(4) ≥ 84 and Σ(4) ≥ 11.[1] (TODO: the abstract says "or ≥ 12 using a different stopping convention")
- 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).[2]
- In 1974, Allen Brady proves that S(4) = 107.[3] (better source needed)
- In 1983, Allen Brady publishes the proof that Σ(4) = 13 and S(4) = 107. [4] 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."[1]
- In 2024, S(4) = 107 was confirmed as part of Coq-BB5. [5]
References
- ↑ 1.0 1.1 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
- ↑ 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.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
- ↑ 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/
- ↑ https://github.com/ccz181078/Coq-BB5/blob/main/BB42Theorem.v