Difference between revisions
busy-beaver-5
Status and infobox
- status:
—→ solved - tier:
—→ V3 - kind:
—→ problem - year:
—→ 1962 - statement:
—→ What is the maximum number of steps a halting 5-state, 2-symbol Turing machine can run?
Relations
- + related to busy-beaver-6: The original curation links this problem to Busy Beaver BB(6); the argument for the link has not been written yet.
Source +30 −0
+---
+title: Busy Beaver BB(5)
+kind: problem
+status: solved
+tier: V3
+year: 1962
+authors: Tibor Radó
+statement: What is the maximum number of steps a halting 5-state, 2-symbol Turing machine can run?
+space: algorithms
+---
+The answer is 47,176,870. A volunteer collaboration decided whether each of roughly 180 million machines halts, and the whole argument was checked in Coq. It combines a mathematical result, a large computer search and a formal proof, the pattern this atlas is built for. BB(6) is at least beyond 2↑↑↑5 and may run into problems like Collatz.
+
+*Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.*
+
+Posed 1962, Tibor Radó. Closed 2024, the bbchallenge collaboration; proof checked in Coq.
+
+## What would settle it
+
+Coq proof of BB(5) = 47,176,870
+
+## Related problems
+
+- The original curation links this problem to [[related::Problem:busy-beaver-6|Busy Beaver BB(6)]]; the argument for the link has not been written yet.
+
+## Sources
+
+- [Wikipedia: Busy beaver](https://en.wikipedia.org/wiki/Busy_beaver)
+- [bbchallenge.org](https://bbchallenge.org/)
+
+[[Space:algorithms|Algorithms]] · [[Continent:computation|Computation]]
Revision 66 as rendered
The answer is 47,176,870. A volunteer collaboration decided whether each of roughly 180 million machines halts, and the whole argument was checked in Coq. It combines a mathematical result, a large computer search and a formal proof, the pattern this atlas is built for. BB(6) is at least beyond 2↑↑↑5 and may run into problems like Collatz.
Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.
Posed 1962, Tibor Radó. Closed 2024, the bbchallenge collaboration; proof checked in Coq.
What would settle it
Coq proof of BB(5) = 47,176,870
Related problems
- The original curation links this problem to Busy Beaver BB(6); the argument for the link has not been written yet.