Logical independence

A chart showing which busy beaver numbers are independent of theories. Modification of a chart from a Vsauce video.

For any recursively enumerable and arithmetically sound axiomatic theory T, there exists an integer $N_T$ such that T cannot prove the values of BB(n) for any $n\ge N_T$. For Zermelo–Fraenkel set theory (ZF), this value is known to be in the range:

$$6\le N_{ZF}\le 432$$

This lower bound comes from the fact that BB(5) has been proven in Rocq. The upper bound comes from an explicit TM which enumerates all possible proofs in ZF and halts if it finds a proof 0 = 1. Assuming ZF is consistent and sound, then it cannot prove whether or not it is consistent, hence it cannot prove whether or not this specific TM halts.

Harvey Friedman spoke of embedding consistency statements within turing machines in a 2004 posting on the "Foundations of Mathematics" mailing list. Scott Aaronson conjectured in his Busy Beaver Frontier survey that $N_{ZF}\le 20$ and $N_{PA}\le 10$, where $PA$ refers to the theory of Peano Arithmetic. Aaronson also mentioned how if BB(n) is independent of some formal theory T for a value n, the theory $PA$ + “BB(n) = b” can prove the consistency of T, where b is the true value of BB(n).

Axiom of Choice

Due to Shoenfield's absoluteness theorem, it is known that any TM proven non-halting in ZFC can also be proven non-halting in ZF (and the converse is trivially true), therefore

$$N_{ZFC}=N_{ZF}$$

Therefore we refer to ZF and $N_{ZF}$ throughout this article since adding the Axiom of Choice does not have any effect on Turing machine decidability.

History

There is no one authoritative source on the history of TMs independent of ZF, this is our best understanding of the history of TMs found. Mostly these are taken from Scott Aaronson's blog announcements and Busy Beaver Frontier or self-reported by the individuals who discovered them. The Aaronson-Yedida machine used a compiler called Laconic, which was then updated with NQL or "Not Quite Laconic", while the current champion machines use a compiler built by Andrew J. Wade.

Note that these results also have not undergone formal verification, with the 7910 machine in particular relying on a result from Harvey Friedman that has no published proof.

History of ZF independent TMs

States	Date	Discoverer	Source	Verification
7910	May 2016	Adam Yedidia and Scott Aaronson	Yedidia and Aaronson 2016
748	May 2016	Stefan O’Rear	Github NQL file, Busy Beaver Frontier
745	July 2023	Johannes Riebel	Riebel 2023 Bachelor Thesis
643	July 2024	Rohan Ridenour	Github NQL, Aaronson Announcement
636	31 August 2024	Rohan Ridenour	Github NQL (commit)
588	12 July 2025	Andrew J. Wade	Github NQL (commit)
549	16 July 2025	Andrew J. Wade	Github NQL (commit)
432	19 Aug 2025	Andrew J. Wade	git commit

Wade's 432-state champion also omits the axiom of regularity.

For Peano Arithmetic, the ZF independent machines are an upper bound. In general, a machine that is independent of a theory will also be independent of any theory with strictly lower consistency strength. For the theories in this article, Con(ZFC+Subtle)->Con(ZFC)->Con(PA).

History of Peano Arithmetic (PA) independent TMs

States	Date	Discoverer	Source	Verification
372	11 February 2026	@LegionMammal978	Github

This machine takes Wade's ZF champion and replaces the set theory axioms with one axiom schema of "adjunction + separation", which has been shown to interpret PA.

Large cardinals

These tables are for theories stronger than ZFC.

History of ZFC + "There exist arbitrarily large subtle cardinals" independent TMs

States	Date	Discoverer	Source	Verification
493	25 February 2026	@LegionMammal978	Github

This machine takes Wade's ZF champion and adds the axiom of Choice and a statement from Harvey Friedman (Proposition 4.3 of "Primitive Independence Results") which Friedman showed with ZFC to be equivalent to "There exist arbitrarily large subtle cardinals".

For reference, this theory is between the strength of "strongly unfoldable" and "$0^{\mathrm{♯}}$ exists" on the large cardinal hierarchy on Wikipedia.

Note: The initial machine produced in 2016 by Yedidia and Aaronson is designed to halt iff a certain statement created by Harvey Friedman is true. According to Friedman (without a published proof), this statement is independent of the theory "Stationary Ramsey Property" or SRP, which is equiconsistent with the theory $ZFC+\{\text{``There is a }k\text{-subtle cardinal``}\mid k\in \mathbb{\mathbb{N}}\}$ which is also between the strength of "strongly unfoldable" and "$0^{\mathrm{♯}}$ exists" on the large cardinal hierarchy. However, the theory used by the BB(493) machine is also independent of this theory.