Independence Impedance

$BB(n)$ is the largest number of steps that any halting Turing machine takes, in the following TM model

• $n \in \N_+$ states plus a halt state
• Two-way unbounded tape
• Binary alphabet

To show $BB(n) = k$ we need to show $BB(n) \geq k$ and $BB(n) \leq k$. The first, by showing there is an $n$-state TM that halts after $k$ steps; the second, by showing there is no halting $n$-state TM that runs for more than $k$ steps.

Note that the witness to the lower bound, “$M$ halts in $k$ steps for some halting $n$-state TM”, is in $\Delta_0$, and the lower bound itself, $BB(n) \geq k$, needs a $\Sigma_1$ formula. This is fine in ZFC and even Robinson arithmetic, both of which are $\Sigma_1$-complete.

For the upper bound, consider the set $\mathscr{M}$ of $n$-state TMs, still in our friendly old model, and consider the (uncomputable, metatheoretic) partition $\mathscr{M} = \mathscr{H} \oplus \overline{\mathscr{H}}$ of $\mathscr{M}$ into the set $\mathscr{H}$ of halting TMs and the set $\overline{\mathscr{H}}$ of nonhalting TMs. Each machine $M \in \mathscr{H}$ halts at most some $k$ steps. Therefore ZFC can prove the runtime of each machine in $\mathscr{H}$. What about $\overline{\mathscr{H}}$? If ZFC could prove $BB(n) \leq k$, then for each $M \in \overline{\mathscr{H}}$, ZFC could prove that $M$ does not halt, just by running each of them for $k + 1$ steps and noticing that it doesn’t halt. In the other direction, if ZFC could prove that $M$ does not halt for each $M \in \overline{\mathscr{H}}$, then it could use the haltingness of each $M \in \mathscr{H}$ to show $BB(n) \leq k$. I.e.,

If ZFC is consistent then we can write such a program $M^\ast$, which $M^\ast$ does not halt but whose nonhalting ZFC cannot prove. In particular, let $M^\ast$ be the machine that loops over all ZFC proofs and, for each one, checks if it is a syntactically valid proof of some contradiction like $0 = 1$ and halts (accepts) iff so. $M^\ast$ will never halt, of course, assuming ZFC is consistent; but ZFC cannot prove this, by Godel’s 2nd incompleteness theorem. Further, if $M^\ast$ requires $n_0$ states, then for $n \geq n_0$, we can extend $M^\ast$ to a machine with $n$ states (e.g. by padding with $n - n_0 \geq 0$ unreachable states) that ZFC cannot prove to be nonhalting but that we know to be nonhalting. This would mean that ZFC could not prove an upper bound on $BB(n)$. In fact, in the other direction, if ZFC can prove $BB(n_0) = k$, then we could just run $M^\ast$ for $k + 1$ steps, and if it didn’t halt then not only would we know that ZFC were consistent (because otherwise $M^\ast$ would have halted upon finding a syntactically valid proof of a contradiction like $0 = 1$) — we would know that ZFC could use the (finite) history of $M^\ast$ to prove this fact, i.e. its own consistency.

In other words, by incompleteness, ZFC cannot prove $BB(n_0) = k$, so there is a model $\mathcal{M} \models \text{ZFC}$ of ZFC in which $BB(n_0) \neq k$. ZFC can prove $BB(n_0) \geq k$, so $\mathcal{M}$ must have $BB(n_0) > k$. But $\mathcal{M}$ is checking the same $n_0$-state TMs as the standard model $\N$ and agrees with $\N$ on the first $k$ steps (i.e. in finding no contradiction). Eventually though they disagree because of nonstandard integers $H \in \N^{\mathcal{M}}$ that are larger than every standard finite number $0, 1, \ldots, k, \ldots$. Namely, in a model like $\mathcal{M} \models \text{ZFC} + \neg \text{Con}(\text{ZFC})$, $M^\ast$ runs for a nonstandard number $H > \N$ of steps, finds a proof of $0 = 1$ with nonstandard length, and evaluates $BB(n_0)$ to $H > k$.

Coming down to earth from these lofty nonsensical nonstandardness things, in good old-fashioned traditional home-style authentic genuine ZFC, we know $BB(1), \ldots, BB(5)$ exactly, and we have a few-hundred-state TM for $M^\ast$. This $M^\ast$ machine keeps shrinking, so just say it has $n_0$ states. Between 6 and $n_0$ states, maybe we can also get independence of ZFC? We got $BB(n_0)$ unprovable by ZFC by somehow encoding into it the inconsistency of ZFC. Without doing that, Who knows; for now, we diagonalize.

[ human ]

give a timeline of busy beaver numbers known to be independent of ZFC

[ alien ]

As of October 21, 2026, the smallest bound I found is BB(230), from Elliot Glazer’s newly released construction. Its verification includes the crucial result that PA proves the machine’s nonhalting equivalent to Con(ZFC). K230 project

These are progressively smaller indices n beyond which ZFC cannot establish concrete Busy Beaver values. I use the standard convention: n working states including the initial state, with the halt state excluded.

Date	Bound reached	Researchers and development
May 2016	7,918 → 7,910	Adam Yedidia and Scott Aaronson. First explicit bound, encoding a statement from Harvey Friedman. Establishing actual nonhalting used a stronger, large-cardinal consistency assumption. Initial announcement, paper
May 2016	1,919	Stefan O’Rear. Directly searches for a contradiction in set theory, removing the stronger consistency assumption. O’Rear’s announcement
2017	748	O’Rear. Further simplification of the proof enumerator and compiler. Some timelines incorrectly date this improvement to 2016. Construction, Riebel’s historical account
March 2023	745	Johannes Riebel. Three-state improvement, documented in his thesis; explicitly conditional on correctness of the compiler and code. Thesis
July 2024	643	Rohan Ridenour. Further compiler improvements. Announcement
August 2024	636	Ridenour. Improved handling of a register-machine instruction. Commit
July 2025	588 → 549	Andrew J. Wade. Removed unnecessary transitions and improved instruction alignment. 588-state commit, 549-state commit
August 2025	432	Wade. New compilation framework. Construction history
August 2026	393	Wade. Further framework and axiom-order optimizations. Dated source
October 10–11, 2026	361 → 354 → 336 → 335	Jeffrey Ketchersid, using Claude agents. Program and axiom simplifications, accompanied by Coq proofs connecting machine halting to inconsistency of ZFC. Constructions and verification
October 13–14, 2026	254	Mira / Mira-Cult, with formal verification by Ketchersid. Verified construction
October 19–20, 2026	230	Elliot Glazer. Rocq verification of the machine’s behavior, followed by verification that the relevant equivalence is provable in PA. K230

There was also a 253-state reduction submitted October 15 by mira-emmy. Its author explicitly limits the verified claim to the external halting/contradiction equivalence, without claiming formalized independence or internal provability, so it deserves that qualification. Submission

Two logical qualifications matter:

• Consistency versus independence: for the direct consistency-search constructions, consistency of ZFC suffices to rule out every provable numerical upper bound. To conclude that the true equality $BB(n)=k$ is neither provable nor refutable, Σ₁-soundness suffices.
• Each bound covers all larger indices. Thus the latest construction gives the upper bound $N_{\text{ZFC}} \leq 230$; together with the established value of BB(5), the current range is $6 \leq N_{\text{ZFC}} \leq 230$ under those assumptions. Proof of (BB(5)), K230