Smallest $n$ for which the value of $BB(n)$ is undecidable

Description of constant

$C_{14}$ is the smallest $n$, such the the value of the busy beaver number $BB(n)$ is undecidable in ZFC (or equivalently ZF). Explicitly, it is the smallest $n$ such that there is a Turing machine with $n$ states for which it cannot be proven in ZFC (assuming ZFC is consistent) whether it halts or not.

The existence of $C_{14}$ essentially follows from Gödel’s second incompleteness theorem and the fact that Turing machines are strong enough to encode ZF.

Known upper bounds

Bound	Reference	Comments
7910	[YS2025]	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 $BB(3)$
5	[B1983]	By computing $BB(4)$
6	[BB2025]	By computing $BB(5)$

Additional comments

Scott Aaronson conjectured in [S2020] that $C_{14} \leq 20$.
A discussion of this topic can be found in the “Independence of ZFC” entry in the Busy Beaver Challenge Wiki.

References

[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