User:GregoryMorse/Computability and provability guide

Computability and provability ask different questions: what an algorithm can determine, and what a specified axiom system can prove. This guide connects those questions to Busy Beaver, Beeping Busy Beaver, halting, consistency and common misconceptions.

For machine notation and the basic game, start with Introduction to the Busy Beaver Function. For up-arrows and fast-growing hierarchies, see Measuring large numbers. This guide uses BB for the maximum-runtime function, rather than the maximum number of printed 1s.

The essential distinction An undecidable problem has no algorithm that always gives the correct answer on every input. A statement independent of a theory has neither a proof nor a disproof in that theory. An unresolved machine is simply one whose behavior is not yet known.

1. Start here: four different questions

Question	Appropriate concept	What it does not imply
Can this particular machine be simulated?	Execution	That its eventual behavior can be recognized in finite time.
Do we currently know its behavior?	Resolved / unresolved; holdout	That an unresolved case is independent of PA or ZFC.
Can one algorithm settle every instance in a specified family?	Algorithmic decidability	That every individual instance is mysterious.
Can a specified axiom system settle a specified statement?	Provability / logical independence	That the statement has no truth value in the standard natural numbers.

The two common meanings of undecidable are therefore:

• Algorithmically undecidable: no total computable procedure decides all inputs of the problem.
• Undecidable in a theory $T$: neither $T⊢\phi$ nor $T⊢\mathrm{\neg }\phi$. This is also called independence from $T$.

Always specify the input family in the first usage and the theory in the second. Uncomputable and incomputable are synonyms: a function has no algorithm that returns its value on every input. The characteristic function of a decision problem connects these notions: it is computable exactly when the problem is decidable.

2. What actually happens when a machine is run?

For a deterministic machine with its initial tape fixed, the mathematical execution has exactly one of two outcomes:

Execution	What finite observation establishes	What remains
It halts after $t$ steps	A finite execution witnesses halting.	The trace may be too long to store; a proved acceleration can provide a shorter certificate.
It never halts	Simulating any finite number of steps establishes only that it has not halted yet.	A separate argument may prove nonhalting: a loop, invariant, unreachable halt, or another mathematical reason.

There is no special physical event called “becoming undecidable.” The transition rules continue to apply normally. The limitation concerns what an algorithm or a proof system can establish about the execution.

A machine whose blank-tape halting statement is independent of a theory extending ordinary arithmetic must actually be nonhalting. If it halted after a standard finite number of steps, that finite fact would be provable in basic arithmetic. Its nonhalting may nevertheless be provable in a stronger theory. “Impossible to prove” must always name the permitted axioms.

Example. A program that moves right forever is nonhalting and easy to analyze. A program that searches for a contradiction in ZFC is also nonhalting if ZFC is consistent, but proving that requires a very different argument. Identical outcomes can have very different proof requirements.

3. BB is a finite maximum, but its whole sequence is uncomputable

Fix the model: one two-way infinite tape, two symbols, blank input, $n$ working states and a separate halt state. Count the halting transition as a step. In this guide:

$$\mathrm{B}\mathrm{B}(n)=\max \{t(M):M\text{ has at most }n\text{ working states and halts from blank tape}\}.$$

Allowing unreachable states makes “at most $n$” equivalent to “exactly $n$” under these conventions. The step-count function is often written $S(n)$; the maximum number of 1s left on the tape is a different function, $\mathrm{\Sigma }(n)$. Check conventions before comparing records.

There are finitely many machines of each size. Every halting one has a finite runtime. Their maximum is therefore a well-defined finite integer. Nonhalting machines are excluded from the maximum; they do not give BB the value infinity.

Finite object	Infinite uniform task
A particular $\mathrm{B}\mathrm{B}(n)$ is an integer.	The function $n\mapsto \mathrm{B}\mathrm{B}(n)$ requires answers for every size.
A fixed finite set of blank-tape machines has a finite table of correct halting answers.	There is no effective procedure that constructs those tables correctly for all sizes.
A correct table can be hardcoded into a program.	Existence of such a program does not tell us which table to hardcode.

Why computing BB would solve halting. Given any program and finite input, effectively compile them into a blank-tape binary machine with $m$ states. Obtain $\mathrm{B}\mathrm{B}(m)$ and simulate that many steps. If the machine has not halted, it never will. Thus a total BB algorithm would decide the general halting problem. Conversely, a halting oracle can classify the finitely many machines of each size, run the halters, and take their maximum.

In computability notation, $\mathrm{B}\mathrm{B}{\equiv }_T{0}^{\prime }$: BB and the halting problem compute each other using oracles. This compares information, not practical running time. A logical oracle is additional information supplied by definition; it is not obtained merely by running a large simulation or using a stronger heuristic.

Growth: the quantifiers matter

For every total computable function $f:\mathbb{\mathbb{N}}\to \mathbb{\mathbb{N}}$, BB eventually exceeds it:

$$\mathrm{\forall }f\text{ total computable}\mathrm{\exists }N\mathrm{\forall }n\ge N:\mathrm{B}\mathrm{B}(n)>f(n).$$

This is stronger than saying “its values are enormous.” Towers, Ackermann-style functions and other computable growth rates remain computable. The domination theorem itself proves BB uncomputable: otherwise take $f(n)=\mathrm{B}\mathrm{B}(n)+1$.

There is no computable upper bound valid for every $n$, or even for all sufficiently large $n$. Bounds on particular finite ranges are possible. Conversely, uncomputability need not involve fast growth: the 0-or-1 characteristic function of halting is already uncomputable.

Approximating BB does not tell us when to stop

Run every machine of size at most $n$ for $s$ steps. Let $L_s(n)$ be the largest runtime among the halts seen, or zero if none has been seen. This is a computable, nondecreasing lower approximation, and

$$\underset{s\to \mathrm{\infty }}{\lim }{L}_s(n)=\mathrm{B}\mathrm{B}(n).$$

For each fixed $n$, the approximation eventually becomes correct permanently. An effective rule that always recognized that point would compute BB. Convergence without a computable stopping certificate is not an algorithm for the exact answer.

4. Encoding halting is possible; deciding every encoding is impossible

Encoding preserves a question. A decision procedure answers it. Replacing a program with a number, equation, optimization problem or another machine does not automatically supply a way to decide its behavior.

Programs, inputs and finite execution histories can all be encoded as integers. Arithmetic can express “there exists a valid halting history.” The Davis–Putnam–Robinson–Matiyasevich theorem gives an effective encoding into polynomial equations with integer coefficients:

$$M\text{ halts}⟺\mathrm{\exists }{x}_1,\dots ,x_r\in \mathbb{\mathbb{N}}:P_M(x_1,\dots ,x_r)=0.$$

What does not exist is an algorithm deciding solvability for every such equation. A formalized proof of this encoding and undecidability is available.

The domain matters: unbounded integer solutions, rational solutions, real solutions and bounded integer solutions are different problems. “It is polynomial” does not identify an available decision algorithm. A finite, explicitly bounded search is decidable, possibly impractically large.

A universal machine encodes arbitrary programs on its input tape. That tape varies through infinitely many possibilities. One fixed universal machine on one fixed blank tape has only one execution. Universality therefore does not create a smallest state count at which the finite blank-tape problem becomes algorithmically undecidable.

5. PA, ZF, ZFC and Gödel's two incompleteness theorems

Name	What it supplies	Consistency versus truth
PA — first-order Peano arithmetic	Axioms for natural-number arithmetic, with induction for every first-order arithmetic formula.	“Consistent” means no contradiction is derivable. It does not by itself mean every theorem is true of the standard natural numbers.
ZF — Zermelo–Fraenkel set theory	A set-theoretic foundation in which arithmetic and much more can be developed.	A theory is a collection of axioms, not itself a model.
ZFC	ZF with the axiom of choice.	Greater set-theoretic proving power does not automatically give greater proving power for arithmetic sentences.
NF — Quine's New Foundations	A different set theory, based on stratified comprehension.	“Weaker” needs a specified comparison: theorem inclusion, interpretation and consistency strength are different relations. NF is not simply ZFC with some axioms removed.
Arithmetical soundness	Every arithmetic theorem of the theory is true in the standard natural numbers.	Stronger than consistency. For many halting arguments, the relevant weaker requirement is ${\mathrm{\Sigma }}_1$-soundness: no false existential computational claim is proved.

Gödel's first incompleteness theorem, in its Gödel–Rosser form, says that a consistent, effectively axiomatized theory containing sufficient arithmetic is incomplete: some sentence has neither a proof nor a disproof in it.

Gödel's second incompleteness theorem says, for such a theory with the usual arithmetized proof predicate and the standard derivability conditions:

$$\mathrm{Con}(T)⟹T⊬\mathrm{Con}(T).$$

Here $\mathrm{Con}(T)$ expresses that no finite $T$-proof of a contradiction exists. The theorem concerns an internal derivation. It does not prohibit a consistency proof using principles unavailable in $T$.

For example, ZFC proves the consistency of PA. Gentzen's consistency proof for PA uses transfinite induction up to ${\epsilon }_0$ in an appropriate weak base; the additional induction principle is the crucial resource. Neither contradicts Gödel.

Choice and blank-tape arithmetic. ZF and ZFC have the same arithmetic consequences. The standard argument uses the constructible universe $L$: it satisfies choice and has the same natural-number arithmetic. Consequently adding choice does not settle additional fixed halting statements over ZF. This is a specific conservativity fact, not a rule saying all extra axioms are irrelevant.

6. The consistency-checking machine: a three-layer argument

Construct $C_T$ to enumerate candidate finite proofs, check them, and halt if it finds a $T$-proof of a contradiction. For an effectively enumerable axiom system, axiom-enumeration witnesses can be included in the certificates.

Layer	Claim	What is needed
1. Program correctness	$\mathrm{Halt}(C_T)\leftrightarrow \mathrm{\neg }\mathrm{Con}(T)$	A faithful proof encoding, enumeration and machine implementation.
2. Internal correctness	$T⊢(\mathrm{Nonhalt}(C_T)\leftrightarrow \mathrm{Con}(T))$	The required comparison must be provable inside $T$; a proof in a stronger metatheory is not automatically this claim.
3. Unprovability	If $T$ is consistent, $T⊬\mathrm{Nonhalt}(C_T)$.	Apply Gödel's second theorem to the internal comparison.

The two actual behaviors are transparent:

                  enumerate and check candidate proofs
                                 |
                    +------------+------------+
                    |                         |
              no contradiction          a contradiction
                proof exists             proof exists
                    |                         |
               run forever               eventually halt
                    |                         |
             T is consistent            T is inconsistent

No amount of unsuccessful finite searching proves that there is no contradiction proof. If the machine genuinely halts, the accepted proof must be extracted and checked against the intended axioms. A simulator or compiler error is not an inconsistency in mathematics.

Watch for an extra “proof of.” Searching for a $T$-proof of $0=1$ and searching for a $T$-proof of “$T$ is inconsistent” are different tasks. The latter searches for a proof of an existential claim about proofs. It does not necessarily extract an actual contradiction proof. Read the formal endpoint before replacing either description with the other; consistency alone does not rule out the latter search succeeding in an unsound theory.

One-sided unprovability is not automatically independence. Consistency alone yields the nonhalting unprovability above. To also exclude a false $T$-proof of “this machine halts,” assume suitable ${\mathrm{\Sigma }}_1$-soundness, or establish that second direction separately. A consistent theory can falsely believe that it has a contradiction proof. In particular, if PA is consistent, $\mathrm{P}\mathrm{A}+\mathrm{\neg }\mathrm{Con}(\mathrm{P}\mathrm{A})$ is a standard example of a consistent but arithmetically unsound theory.

Why this produces a theoretical bound on provable BB values

Suppose $C_T$ has $m$ working states, its correctness is internally available, and $T$ is consistent. For any standard numeral $b$:

          T proves BB(m) <= b
                    +
    a checked finite trace: C_T has not halted by b
                    |
                    v
          T proves C_T never halts
                    |
                    v
             T proves Con(T)
                    |
                    v
          forbidden by Gödel's second theorem

The finite trace exists because consistency makes $C_T$ genuinely nonhalting. Thus $T$ cannot prove any numerical upper bound for $\mathrm{B}\mathrm{B}(m)$, and in particular cannot prove an exact numerical value. Padding carries the obstruction to larger state counts.

This is a theoretical, conditional upper bound on what $T$ can prove, not merely a practical difficulty. It is neither a value of BB nor necessarily the first state count where $T$ fails. A recent fully internalized project also reports the BB nonprovability conclusion itself as a checked theorem.

7. “A formula for BB up to k”: three different claims

Claim	Status	Where the information is
For every fixed finite $k$, some polynomial matches $\mathrm{B}\mathrm{B}(1),\dots ,\mathrm{B}\mathrm{B}(k)$.	True.	Its coefficients can contain the entire finite answer table.
One algorithm produces a correctly evaluable formula for every prefix length $k$.	Impossible, if evaluation is uniformly effective and exact.	Such an algorithm would compute $\mathrm{B}\mathrm{B}(k)$.
A short logical definition specifies BB for all $n$.	True.	The definition contains an unbounded halting condition; it does not provide a terminating evaluator.

There is no largest finite $k$ for which some polynomial exists. The quantifier order is

$$\mathrm{\forall }k\mathrm{\exists }{P}_k\mathrm{\forall }i\in \{1,\dots ,k\}:P_k(i)=\mathrm{B}\mathrm{B}(i).$$

This does not give a computable map $k\mapsto P_k$. The following constructions make the distinction explicit; they assume the correct finite values have already been supplied.

Four ways to repackage a supplied finite table

Let $b_i=\mathrm{B}\mathrm{B}(i)$ for $1\le i\le k$.

Polynomial interpolation. Lagrange interpolation gives a rational-coefficient polynomial of degree at most k − 1:

$$P_k(x)=\sum _{i=1}^k{b}_i\prod _{1\le j\le k,j\ne i}\frac{x-j}{i-j}.$$

At x = i, the i-th basis product is 1 and every other basis product is 0. Therefore P_k(i) = b_i. The formula exists even when we do not know its coefficients numerically. Multiplying by a common denominator gives an integer-coefficient relation, not necessarily an integer-coefficient polynomial with the same outputs.

Piecewise functions and linear interpolation. Return $b_i$ when the input is $i$. Alternatively, join consecutive points by line segments. Both reproduce the supplied samples; neither justifies extrapolation. For illustration, the line through $(1,1)$ and $(2,6)$ is $5x-4$. It matches those BB values but predicts 11 at 3, whereas $\mathrm{B}\mathrm{B}(3)=21$.

A linear encoding with binary selectors. For the bounded domain, introduce ${\delta }_i\in \{0,1\}$ and impose

$$\sum _i{\delta }_i=1,x=\sum _{i}i{\delta }_i,y=\sum _i{b}_i{\delta }_i.$$

These linear constraints represent exactly the listed pairs. The values are still present as coefficients. Dropping the integrality requirement would instead allow fractional mixtures and would change the represented set.

Quadratic constraints with auxiliary variables. A finite polynomial evaluation circuit can replace each multiplication by $z=uv$ and each addition by $z=u+v$. This gives a system of equations of degree at most two, using more variables. It does not create a general solver or reveal unknown coefficients. A single quadratic objective, a quadratic equation system, and a QUBO formulation have different requirements; bounds and penalty choices must be justified. Slack variables can encode appropriate inequalities, but do not in themselves encode arbitrary products.

Three “cutoffs” that must not be confused

Object fixed in advance	Meaning of a cutoff
One particular total computable candidate $f$	It must disagree with BB somewhere. Its first disagreement is a finite, candidate-dependent index; it need not be effectively recognizable. Eventual domination also means it agrees at only finitely many indices.
One fixed theory $T$	There is a bound beyond which true exact numerical BB equalities are unprovable, under the hypotheses above. Explicit consistency machines can give theoretical upper bounds on this proof limitation.
A formula class plus explicit size/resource limits	Which prefixes can be represented, discovered or certified depends on the class and limits. “Closed form” alone does not specify them.
All finite formulas, with no size limit	There is no finite maximal prefix length: tables and interpolation work for every fixed finite prefix.

Independence can prevent $T$ from certifying that a particular supplied table is correct. It cannot prevent that table, or its interpolating polynomial, from existing. Nonuniform existence, effective discovery and proof of correctness are three different questions.

8. BBB: the last beep need not be a halt

A beeping machine has a designated event, such as entering a particular state. Let $b(M)$ be the time of its last beep if it beeps finitely often, and infinity if it beeps infinitely often. Set $b(M)=0$ when it never beeps. With a fixed event and step convention,

$$\mathrm{B}\mathrm{B}\mathrm{B}(n)=\max \{b(M):M\text{ has at most }n\text{ states and }b(M)<\mathrm{\infty }\}.$$

Such a machine quasihalts when it stops beeping forever. Its ordinary execution can continue forever after that event. Both beep-state and beep-transition variants are called BBB on this wiki. Label the observer explicitly when comparing state counts or exact values; one may write “BBB(18), beep transition” or “BBB(19), beep state”. Entering versus leaving a state also requires a consistent time convention.

 ordinary halt:        step -- step -- HALT
 finite beeping:       beep -- beep -- LAST BEEP -- step -- step -- ...
 infinite beeping:     beep ----- beep -------- beep ------- beep -- ...

A finite pause alone does not certify “last beep”. Even if the exact value $B=\mathrm{B}\mathrm{B}\mathrm{B}(n)$ is supplied, simply simulating to time $B$ does not decide whether an $n$-state machine quasihalts: an infinitely beeping run may have a long gap across that time. A beep strictly after $B$ certifies infinitely many beeps, because a finitely beeping machine cannot have its last beep later than the bound. Establishing permanent silence still needs an argument or additional information, such as a halting oracle answering whether a later beep occurs.

The underlying quantifiers are:

Question	Logical shape	Level
Does an ordinary machine halt?	$\mathrm{\exists }t:\mathrm{HaltBy}(M,t)$	${\mathrm{\Sigma }}_1^0$-complete as a general decision problem.
Does it never halt?	$\mathrm{\forall }t:\mathrm{\neg }\mathrm{HaltBy}(M,t)$	${\mathrm{\Pi }}_1^0$-complete.
Does it beep finitely often?	$\mathrm{\exists }t\mathrm{\forall }s>t:\mathrm{\neg }\mathrm{BeepAt}(M,s)$	${\mathrm{\Sigma }}_2^0$-complete.
Does it beep infinitely often?	$\mathrm{\forall }t\mathrm{\exists }s>t:\mathrm{BeepAt}(M,s)$	${\mathrm{\Pi }}_2^0$-complete.

BB has halting-oracle degree $0^{\prime }$; BBB has the next-jump degree $0^{″}$. BBB remains uncomputable even with an oracle for BB. In the standard model it eventually dominates every total function computable using that oracle, rather than merely being a fixed iterate such as $\mathrm{B}\mathrm{B}(\mathrm{B}\mathrm{B}(n))$.

Example: twin primes. Enumerate primes and beep whenever a new twin-prime pair is found. Infinitely many twin primes means infinitely many beeps; finitely many means quasihalting. This construction does not solve the twin-prime conjecture. It explains why the acceptance condition needs more than ordinary finite-witness halting.

BBBB and beyond. Beeping–booping variants add a further recurrence condition, rather than just another sound. Current proposals count outputs between boops and examine values recurring infinitely often. Exact definitions matter; higher oracle busy-beaver functions provide a systematic hierarchy. Do not assume the number of letters alone fixes a mathematical model.

9. What practical BB research proves

Observation or result	What it establishes	What it does not establish
A proved halter with runtime $r$	$\mathrm{B}\mathrm{B}(n)\ge r$.	That it is the champion among all machines.
All machines covered by sound analysis; maximum halting runtime $r$	$\mathrm{B}\mathrm{B}(n)=r$.	A general BB algorithm.
A verified nonhalting invariant	Nonhalting of the machines covered by that invariant.	Coverage of machines outside its hypotheses.
A very long simulation with no halt	A finite lower bound on the time before any halt.	Nonhalting, or independence from a theory.
A proved accelerated recurrence	A precise description of execution, for the configurations covered.	That the resulting arithmetic recurrence has been solved globally.
A decider times out or returns “unknown”	That method did not settle this case.	Mathematical undecidability or nonhalting.

In bbchallenge usage, a decider commonly recognizes a useful class of behaviors and can leave other machines unresolved. Several such methods, plus individual proofs, can cover a finite domain. This use of “decider” is compatible with the impossibility of a total universal halting decider.

The BB(5) result demonstrates the distinction: a finite domain was exhausted and the maximum proved, despite the general function being uncomputable. Proofs and certificates can be much shorter than the executions they describe. Finding and checking such a certificate are different tasks.

The winning machine itself halts, so its finite runtime can in principle be proved in elementary arithmetic. The difficult or unprovable claim can instead be its maximality: no other halting machine of that size runs longer. Similarly, ZFC can prove that every BB value exists without proving which standard numeral denotes a particular value. An existential theorem need not supply an individually provable numerical answer.

A brute-force search for an invariant can yield a sound proof; it does not need to find that invariant “intelligently”. The decisive check is that the invariant contains the initial configuration, is preserved by every possible next step, and excludes halting. Agreement with a finite simulated prefix does not establish those closure properties. The same distinction applies to AI-proposed deciders: finding a candidate and validating its soundness are separate tasks.

For a real computer with a fixed, finite bound on memory and no unbounded external input, there are finitely many configurations. Repetition or halting can in principle be detected by exhaustive exploration. This finite-state fact does not make unbounded-memory program halting decidable; nor does it make enormous finite exploration practical.

Generalized Collatz functions: a computable rule can have undecidable reachability

The Generalized Collatz Function page describes maps whose update rule is affine on each residue class modulo a fixed integer. The rational coefficients are chosen so that the updates remain natural numbers. Every individual update is computable. Conway showed how generalized iterations can simulate computation; simplicity of a step rule does not make its long-term behavior uniformly decidable.

Question	Quantifiers	Consequence
Compute the next value, or the value after a supplied finite number of steps.	A finite calculation.	Computable.
Given a generalized rule and a starting value, does the trajectory reach 1?	$\mathrm{\exists }t:g^t(x)=1$	A finite-witness reachability problem; the general family can encode halting.
Given a generalized rule, does every positive starting value eventually reach 1?	$\mathrm{\forall }x>0\mathrm{\exists }t:g^t(x)=1$	The generalized Collatz problem is ${\mathrm{\Pi }}_2^0$-complete, as proved by Kurtz and Simon.
Does the ordinary, fixed $3n+1$ rule reach 1 from every positive start?	One particular universally quantified statement.	Undecidability of the generalized family does not prove this statement independent of PA or ZFC.

The all-input result has a different quantifier pattern from single-input halting. Likewise, deriving a Collatz-like recurrence for a BB machine may transfer the question into arithmetic without answering it. The recurrence, its chosen initial value, its stopping condition and the scope of the proved simulation must all be specified.

10. October–November 2026: records and what their proofs mean

Snapshot: 9 November 2026. This is a selection of relevant developments, not a claim to enumerate every result or identify a permanently current champion. “Repository reports checked” means that the linked project supplies statements and checking information; this guide's preparation did not independently rebuild the proof developments. Counts below mean working states with two symbols unless otherwise stated.

Date / milestone	Construction or result	Evidence and scope
2016: historical starting point	Yedidia–Aaronson's 7,910-state construction gave an explicit ZFC unprovability bound.	Published construction using Friedman's independent combinatorial statements; do not describe it as simply the same direct proof-search program as later machines.
October 2026: PA compression	Mira's 238-state machine; linked Rocq development connects its literal table to finite refutations in ordinary classical PA.	Repository reports a closed endpoint theorem and recursive checking. This external correctness theorem should be distinguished from a separately formalized assertion that PA proves the comparison.
October 2026: 230 states	Elliot Glazer's K230 searches for a ZFC contradiction.	Separate Rocq developments report external correctness and that PA proves the nonhalting/consistency equivalence. The latter uses classical metatheoretic assumptions, explicitly listed, to establish existence of a PA derivation.
21 October 2026: 215 states	Vladimir Reshetnikov's K215 has external Lean and Rocq correctness endpoints.	The pinned README explicitly says this development does not supply an internal PA proof or a derivation in ZFC's proof syntax. This limitation concerns that development, not every project named K215.
Recorded run 23 October 2026: 215 states	Glazer's separate K215 PA/MM0 development reports the internal PA comparison.	Its public specification and receipt describe a checked PA theorem; the project also reports ZFC second-incompleteness and BB(215) nonprovability theorems. Match the literal machine and specification; equal state counts alone do not identify machines.
October 2026: stronger theories	A 296-state construction is linked to ZFC plus “every set lies in a Grothendieck universe.”	The project reports a closed Rocq correctness theorem. This encodes the stronger theory's inconsistency; it does not establish that theory's consistency.
October–November 2026: further compression	Instruction-limited and multisymbol variants trade states, symbols and defined transitions.	Compare like with like. The tinycryptids project documents 469-instruction PA-related and 375-instruction ZFC-related constructions, with explicit qualifications about the equiconsistency bridge and imported proof hypotheses.
9 November 2026: PA, 211 states	The PA211 project publishes a literal blank-tape consistency checker and a Lean independence development.	Under PA consistency it proves nonhalting and that PA cannot prove the exact nonhalting sentence. The two-sided corollary uses a standard model of PA in Lean's metatheory. This is not an internal PA proof of PA consistency; no independent rebuild is claimed here.
Early November 2026: NF, 210 states	A New Foundations consistency machine has a public external Lean development.	The published endpoint reports that, if NF is consistent, NF proves no exact numerical value for BB(210). Two-sided independence of the true value assumes arithmetical ${\mathrm{\Sigma }}_1$-soundness. The package supplies recorded checks; no independent rebuild is claimed here. A PA consequence requires the appropriate additional interpretation or proof-transfer argument.
Reported 8 November 2026: 1,399 states	A ZF + Berkeley-cardinal consistency machine is listed with a Rocq link.	Reported here from the wiki; the linked primary artifact was not accessible during preparation. Berkeley-cardinal claims require attention to choice; do not silently replace this theory by ZFC plus the same axiom.

Recent practical lesson. The 15 October DeepMind preprint reports formally verified Collatz-like accelerations for eleven BB(6) machines while leaving their halting behavior unresolved. That is structural progress, not eleven halting decisions. November's research log also reports finite simulations finally settling the remaining Reus-vampire path on 1 November: very long survival did not imply nonhalting.

For earlier compilation milestones and newer records, consult Logical independence, TMBR: October 2026 and TMBR: November 2026. A historical state count is an upper bound supplied by one construction, not a proof of minimality.

What does 215 bound? Subject to the internal comparison and usual BB formalization, consistency of ZFC implies that ZFC cannot prove $\mathrm{B}\mathrm{B}(n)=b$ for any standard numeral $b$ and $n\ge 215$. Thus a prefix of individually proved exact values cannot extend past 214. This is an upper bound on provability, not a claim that values through 214 are provable or that 215 is minimal. It places no upper bound on the finite prefixes that exist as tables or interpolating polynomials.

11. Reading an alarming “consistency proof” headline

What was actually proved?	Correct interpretation
$\mathrm{Halt}(C_T)\leftrightarrow \mathrm{\neg }\mathrm{Con}(T)$	A correctness/encoding theorem. It leaves the truth of $\mathrm{Con}(T)$ open.
$\mathrm{Con}(S)\Rightarrow \mathrm{Con}(T)$	A relative consistency result; its premise matters.
A stronger theory $S$ proves $\mathrm{Con}(T)$	A consistency proof relative to the principles used in $S$.
$T$ itself allegedly proves its usual $\mathrm{Con}(T)$	If Gödel's hypotheses apply, examine the assumptions, proof predicate, encoding and claimed derivation. A valid such derivation would imply that $T$ is inconsistent.
A concrete finite contradiction proof is found	Check it directly. This is evidence of inconsistency, not just absence of a consistency proof.
“The theorem has no extra axioms” in a proof assistant	An assumption audit within that assistant's foundation. It does not identify the object theory or prove the consistency of the assistant's own foundation.

Fewer machine states measure description length in a specified model. They do not measure the probability of inconsistency, the length of a hypothetical contradiction proof, or the runtime needed to find one.

Why checker sizes can cluster

A proof-search machine must encode both a proof system and the machinery that processes it: pairing and unpairing numbers, manipulating syntax, enumerating candidates, checking inference steps and recognizing axioms. Constructions that reuse the same interpreter can differ mostly in their axiom-recognition code. This can make PA, NF and ZF-related machines close in size even when their theories have different consistency strengths.

This is an implementation explanation, not a theorem imposing a barrier near 200 states. A short description and a strong theory are different properties. A quantifier-free presentation can shift work into combinators or other operators while still interpreting arithmetic; it does not evade incompleteness. Exact state-by-state cost estimates require an actual analysis of the literal machine, rather than an AI-generated breakdown.

What a formalized proof must identify

Check	Why it matters
The exact machine, observer and blank start	A theorem about a prepared tape, a different table or a different beep event may establish a different claim.
The intended mathematical statement	Proving a predicate named “PA consistency” or “P = NP” is useful only after checking what that predicate defines and which assumptions remain.
The object theory and metatheory	Lean can prove a statement about what PA cannot prove. That is a metatheorem, not PA proving its own consistency.

An external Lean theorem can legitimately establish $T⊬\phi$ when it formalizes the relevant derivability claim. An external simulation equivalence alone is a different result. A PA-internal comparison is one way to supply the required bridge, not a universal requirement that every independence proof must take that particular form.

An external proof assistant may reason about all standard finite computations, while an internal PA argument must work in arbitrary models of PA, including nonstandard ones. This explains why the distinction between the two correctness theorems is substantive. A nonstandard model believing that a machine “halts” does not supply a standard finite execution trace.

12. Related results: where they fit

Topic	Connection	Common trap
Goodstein's theorem	Every individual standard Goodstein sequence terminates, but PA cannot prove the universal termination theorem.	Confusing a universal unprovable claim with an individually unprovable finite halt.
Chaitin's $\mathrm{\Omega }$	For an optimal prefix-free universal machine, this halting probability is an uncomputable real; sufficiently many exact initial bits settle corresponding bounded-length halting questions.	Confusing a real's uncomputable infinite expansion with an “uncomputable finite integer,” or treating all choices of universal machine as giving the same bits.
Rice's theorem	Every nontrivial extensional property of the partial computable function computed by an arbitrary program has an undecidable index set.	Applying it to every syntactic question about source code, or forgetting the nontriviality/extensionality conditions.
Proof-theoretic growth	Some total computable functions are not provably total in PA. BB eventually exceeds every total computable function, including those.	Equating “not provably total in PA” with “uncomputable.”
Oracles	An oracle for halting decides ordinary halting; a new halting problem arises for machines equipped with that oracle.	Assuming one oracle decides every level of the hierarchy.
Open mathematical conjectures	A machine can faithfully encode a conjecture without settling it. Existential finite witnesses fit ordinary halting; further quantifier alternations may require other acceptance conditions.	Calling every conjecture-linked machine logically independent of ZFC.

Fixed inputs, totality and the proof-theoretic ordinal

For a computable function, “this run terminates” and “every input terminates” have different logical forms. This is why a fast-growing construction does not automatically give a fixed PA-independent ordinary machine.

Claim	Logical shape	Consequence
A fixed standard input $n$ eventually halts	$\mathrm{\exists }t:\mathrm{HaltBy}(M,n,t)$	If true, its finite trace is provable in elementary arithmetic, however impractically large.
The program halts on every input	$\mathrm{\forall }n\mathrm{\exists }t:\mathrm{HaltBy}(M,n,t)$	A true totality statement can be unprovable in PA even though each fixed-input halt is provable.
A beeper runs inputs in order and beeps after each completed run	Infinitely many beeps iff every input terminates	A verified construction can transfer the totality question to non-quasihalting. It does not produce a finitely beeping numerical BBB champion when the function is total.

In the usual fast-growing hierarchy, ${\epsilon }_0$ is an ordinal index, not a numerical runtime. Its associated diagonal function can be total and computable while its uniform totality is not provable in PA. To obtain a fixed ordinary machine with an unprovable nonhalting statement, one still needs an appropriate finite-witness search and a proved internal connection. Merely writing down a large growth rate, or a long-running halter, does not supply that connection.

13. Quick misconception checklist

If someone says…	Ask or clarify…
“This machine is undecidable.”	Unknown today, outside a particular method, or independent of a named theory?
“It must run forever because the halting problem is undecidable.”	The theorem concerns a family. This instance might halt tomorrow.
“It runs forever, so it must loop.”	An infinite computation can keep changing its tape and never repeat a complete configuration.
“It has run for a huge time, so it cannot halt.”	A finite run gives no general nonhalting guarantee.
“Every individual answer is decidable, so the whole problem is.”	Existence of separate constant-answer programs is not a uniform algorithm.
“BB becomes uncomputable at a particular number of states.”	Uncomputability concerns the infinite function; proof limitations can have theory-relative state bounds.
“A universal machine makes BB undecidable at its state count.”	Arbitrary input and a single blank input are different domains.
“Encoding halting in an equation is impossible.”	Encoding is possible; a universal effective solver is not.
“I found a formula, so I computed BB.”	Are its constants known? Is exact evaluation effective? Is correctness established for all claimed inputs?
“No polynomial can match BB up to a sufficiently large finite k.”	Interpolation works for every finite k; the coefficients may require unknown BB values.
“Linearization or slack variables solve the difficulty.”	Check integrality, bounds, unknown coefficients and whether solving was merely moved to another problem.
“Gödel says consistency cannot be proved.”	It restricts proofs within the theory concerned, under specified hypotheses.
“Gödel's second theorem gives both directions of independence.”	The unprovability of consistency and the unprovability of inconsistency need different hypotheses or arguments.
“A smaller consistency checker is evidence of inconsistency.”	It is a shorter encoding, not a successful contradiction search.
“A machine-checked equivalence proves nonhalting.”	The equivalence still requires the consistency premise to conclude nonhalting.
“A stronger theory's independent statement is automatically independent of any theory with lower consistency strength.”	Use actual theorem inclusion, an appropriate interpretation, or the necessary internally formalized comparison. A bare ranking of consistency strengths is insufficient.
“AI or quantum computing removes the halting obstruction.”	Any proposed effective procedure still faces the same theorem. Practical heuristics and proof search can improve without becoming universal solvers.
“BB encodes every mathematical question.”	Ordinary halting has a specific finite-witness logical form. Higher arithmetic and set-theoretic questions need separate analysis.

14. A precise way to ask for help

For this exact machine and initial tape, do we know whether it halts? Is the claim based on simulation, a mathematical proof, a checked certificate, or an independence theorem? If independent, independent of which theory and under which assumptions?

For a formula claim, add: “What operations and constants are allowed, what is the input range, how is it evaluated exactly, and in which theory is its correctness proved?”

See also

• Introduction to the Busy Beaver Function
• Measuring large numbers
• Logical independence
• Beeping Busy Beaver
• Universal Turing Machine
• Generalized Collatz Function
• Busy Beaver Frontier
• Holdouts
• TMBR: October 2026
• TMBR: November 2026