Smallest for which the value of is undecidable ()
Smallest for which the value of is undecidable: determine or improve its bounds; the repository records 6 (lower) and 432 (upper).
Editorial MSC2020 classification. Original article codes and source evidence are recorded in the literature directory.
Problem statement
is the smallest , such that the value of the busy beaver number is undecidable in ZFC (or equivalently ZF). Explicitly, it is the smallest such that there is a Turing machine with states for which it cannot be proven in ZFC (assuming ZFC is consistent) whether it halts or not.
The existence of essentially follows from Gödel's second incompleteness theorem and the fact that Turing machines are strong enough to encode ZF.
Lean 4
No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.
Background
- Scott Aaronson conjectured in [S2020] that .
- A discussion of this topic can be found in the "Independence of ZFC" entry in the Busy Beaver Challenge Wiki.
References (from the repository page)
- [S2020] Aaronson, Scott. "The busy beaver frontier." ACM SIGACT News 51.3 (2020): 32-54. Available at https://dl.acm.org/doi/pdf/10.1145/3427361.3427369
- [LS1965] Lin, Shen, and Tibor Rado. "Computer studies of Turing machine problems." Journal of the ACM (JACM) 12.2 (1965): 196-212. Available at https://dl.acm.org/doi/pdf/10.1145/321264.321270
- [B1983] A. H. Brady, The determination of Rado's noncomputable function Sigma(k) for four-state Turing machines, Math. Comp. 40 #62 (1983) 647-665. Available at https://docs.bbchallenge.org/papers/Brady1983.pdf
- [BB2025] Blanchard, Justin, et al. "Determination of the fifth Busy Beaver value." 2025. arXiv:2509.12337
- [R2023] Riebel, Johannes. The Undecidability of BB (748). Diss. Bachelor’s thesis, 2023. Available at https://docs.bbchallenge.org/papers/Riebel2023.pdf
- [O2016] Stefan O’Rear. metamath-turing-machines. 2016. See https://github.com/sorear/metamath-turing-machines
- [W2025] Wade, Andrew J. 2025. See https://codeberg.org/ajwade/turing_machine_explorer
- [YS2016] Yedidia, Adam, and Scott Aaronson. "A relatively small Turing machine whose behavior is independent of set theory." 2013. arXiv:1605.04343
Progress & source assessment
Repository table (commit 2c1968c, 26 September 2026): best known lower bound 6; best known upper bound 432. Values marked with an asterisk have minimal verification.
Known upper bounds
| Bound | Reference | Comments |
|---|---|---|
| 7910 | [YS2016] | By reducing to a graph theoretic setting |
| 1919 | [O2016] | By enumerating all proofs in ZF |
| 748 | [O2016] | Proven in 2017 with similar methods |
| 745 | [R2023] | With methods of [O2016] |
| 432 | [W2025] | With methods of [O2016] |
Known lower bounds
| Bound | Reference | Comments |
|---|---|---|
| 4 | [LS1965] | By computing |
| 5 | [B1983] | By computing |
| 6 | [BB2025] | By computing |
- [1]Davis, Damek; Ivanisvili, Paata; Tao, Terence (maintainers). Optimization Constants in Mathematics, github.com/teorth/optimizationproblems (commit 2c1968c, 26 September 2026). — Smallest $n$ for which the value of $BB(n)$ is undecidable ($C_{14}$) linkApache-2.0 (repository license); constant pages reproduced with attribution; repository references retained.
Recorded progress
Add yours →Nothing recorded yet. A pointer to a paper the entry is missing counts.
Machine attempts
0 recordedAttempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.
No machine attempts recorded.
Sign in to run an attempt. New accounts start with enough credits for ten.
Discussion
0 notesNotes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.
No notes yet.
Sign in to add a note.