Measuring Decidability as Related to Busy Beaver Numbers
Pith reviewed 2026-05-21 09:26 UTC · model grok-4.3
The pith
Turing machines that halt exactly when a number-theory conjecture has a new solution classify its decidability by the fewest states required.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
We construct explicit Turing machines that search for a solution to Brocard's problem greater than 7 and a Fermat prime beyond the 4th which halt if and only if such a solution exists. The theoretical existence of Busy Beaver numbers then supplies a new notion of decidability: the minimum number of states needed to model the conjecture gives a classification of the logic system that can describe it.
What carries the argument
Turing machines that search for solutions to a conjecture and halt if and only if one exists, whose state count then ranks the conjecture against Busy Beaver bounds.
If this is right
- Conjectures modelable in few states may fall within the reach of weaker formal systems than those requiring many states.
- The Busy Beaver function supplies an in-principle decision procedure for any such encoded conjecture by providing a finite runtime bound after which non-halting can be certified.
- Explicit machines for Brocard's problem and the search for larger Fermat primes give concrete state-count ranks for those two open questions.
- The same construction technique can be repeated for other unsolved problems to produce comparable state-count classifications.
Where Pith is reading between the lines
- This state-count ranking could be used to order a larger collection of number-theory conjectures and look for correlations with other measures of difficulty such as proof length or axiom strength.
- If smaller machines are found for the same conjectures, the classification would shift toward weaker logic systems, offering a way to refine the measure over time.
- The method highlights a concrete bridge between computability theory and specific arithmetic statements that future work might exploit to obtain conditional non-existence results once partial Busy Beaver values become available.
Load-bearing premise
That representing the existence of a mathematical solution as the halting of a Turing machine, together with the theoretical Busy Beaver function, produces a useful classification of the conjecture's decidability or logical strength.
What would settle it
If the constructed machine for Brocard's problem with k states halts after more than the Busy Beaver number of steps for k states, that would show a solution exists; if it can be shown never to halt within that bound, that would show no solution exists.
Figures
read the original abstract
The theoretical existence of Busy Beaver numbers provides a new notion for decidability and corresponding heuristic for conjectures. The minimum number of states in which a conjecture can be modeled gives a classification of what logic system can describe said conjecture. In this work, we construct explicit Turing machines that search for a solution to Brocard's problem greater than 7 and a Fermat prime beyond the 4th which halt if and only if such a solution exists.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims that the theoretical existence of Busy Beaver numbers yields a new notion of decidability, where the minimum number of states needed to model a conjecture as a Turing machine (that halts iff a solution or counterexample exists) classifies the logical strength or system capable of describing the conjecture. Explicit constructions are provided for two cases: a TM searching for solutions to Brocard's problem (n! + 1 = m² with n > 7) and a TM searching for a Fermat prime beyond the fourth.
Significance. If the central correspondence holds, the work would supply a computability-theoretic heuristic for ranking the decidability of open conjectures via minimal TM state counts, potentially offering a quantitative alternative or complement to proof-theoretic ordinals. The explicit TM constructions for Brocard's problem and Fermat-prime search are a concrete strength that could support further verification or extension.
major comments (2)
- [Abstract and §1] Abstract and opening of §1: the assertion that minimum state count 'gives a classification of what logic system can describe said conjecture' is not backed by any theorem, definition, or explicit mapping from state count to consistency strength, proof-theoretic ordinal, or logical expressiveness; without this, the classification remains informal and does not establish a new decidability measure beyond the known equivalence to halting for that specific machine.
- [§4] §4 (TM constructions): the manuscript asserts explicit machines that halt if and only if a solution exists, yet supplies neither the full state-transition tables, a machine-checked verification, nor an argument that the chosen encoding is minimal or canonical; this is load-bearing because the claimed classification depends on the state count being a well-defined, encoding-independent quantity.
minor comments (1)
- [§2] Notation for Busy Beaver functions and state counts is introduced without a dedicated preliminary subsection; adding explicit definitions and a short comparison to standard BB(n) would improve accessibility.
Simulated Author's Rebuttal
We thank the referee for the careful reading of the manuscript and for the constructive comments, which help clarify the scope of our claims. We respond to each major comment below, indicating where revisions will be made to address the points raised.
read point-by-point responses
-
Referee: [Abstract and §1] Abstract and opening of §1: the assertion that minimum state count 'gives a classification of what logic system can describe said conjecture' is not backed by any theorem, definition, or explicit mapping from state count to consistency strength, proof-theoretic ordinal, or logical expressiveness; without this, the classification remains informal and does not establish a new decidability measure beyond the known equivalence to halting for that specific machine.
Authors: We agree that the manuscript does not contain a formal theorem establishing a direct mapping from minimal state count to consistency strength, proof-theoretic ordinal, or a specific logic system. The central idea is a heuristic: because Busy Beaver numbers are uncomputable, the smallest number of states sufficient to encode a conjecture as a halting problem offers a quantitative proxy for its 'decidability complexity' relative to other conjectures. This is presented as an informal classification inspired by known links between small Turing machines and consistency statements, rather than a proven equivalence. We will revise the abstract and the opening of §1 to remove any phrasing that implies a formal theorem and to state explicitly that the proposed measure is heuristic in nature. revision: yes
-
Referee: [§4] §4 (TM constructions): the manuscript asserts explicit machines that halt if and only if a solution exists, yet supplies neither the full state-transition tables, a machine-checked verification, nor an argument that the chosen encoding is minimal or canonical; this is load-bearing because the claimed classification depends on the state count being a well-defined, encoding-independent quantity.
Authors: The constructions in §4 describe the high-level operation of the machines and report the resulting state counts obtained from standard multi-tape encodings of the respective search procedures. We acknowledge that full transition tables are not supplied in the current text and that no machine-checked verification or formal minimality argument is given. In the revision we will append the complete state-transition tables for both machines. We will also add a short discussion of the encoding conventions used and note that the reported state counts constitute explicit upper bounds rather than proven minimal values; different reasonable encodings may produce modestly different counts, but the relative ordering is expected to be stable. A machine-checked verification lies outside the scope of this theoretical note, but we will release the machine descriptions in a simulator-readable format as supplementary material. revision: partial
Circularity Check
Explicit TM constructions for conjecture searches yield non-circular Busy Beaver-based decidability heuristic
full rationale
The paper constructs explicit Turing machines that search for solutions to Brocard's problem and additional Fermat primes, halting if and only if such solutions exist. It invokes the theoretical existence of Busy Beaver numbers to propose that the minimum state count for modeling a conjecture supplies a classification of the logic system able to describe it. This chain relies on direct construction of the machines and standard properties of Turing machines and the Busy Beaver function; no claimed result reduces by the paper's own definitions or equations to a tautological equivalence with its inputs. The classification is presented as an interpretive consequence of the modeling rather than presupposed by it, and no load-bearing self-citation or ansatz is required for the central steps.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math Busy Beaver numbers exist and grow faster than any computable function.
- domain assumption A conjecture can be modeled as a Turing machine that halts if and only if a solution exists.
Reference graph
Works this paper leans on
-
[1]
A. H. Brady. The determination of the value of rado’s noncomputable functionσ(k) for four-state turing machines.Mathematics of Computation, 40(162):647–665, 1983
work page 1983
-
[2]
H. Brocard. Question 166.Nouvelle correspondance math´ ematique, 2:287, 1876
-
[3]
Richard Crandall and Carl Pomerance.Prime Numbers: A Computational Perspective. Springer, 2 edition, 2005
work page 2005
-
[4]
L. Euler. Observationes de theoremate quodam fermatiano aliisque ad numeros primos spectantibus.Commentarii Academiae Scientiarum Petropolitanae, 6:103–107, 1738
-
[5]
T. Rado. On non-computable functions.Bell System Technical Journal, 41:877–884, 1962
work page 1962
-
[6]
Question 469.Journal of the Indian Mathematical Society, 5:59, 1913
Srinivasa Ramanujan. Question 469.Journal of the Indian Mathematical Society, 5:59, 1913
work page 1913
-
[7]
A relatively small turing machine whose behavior is independent of set theory, 2016
Adam Yedidia and Scott Aaronson. A relatively small turing machine whose behavior is independent of set theory, 2016. Appendices A FP Table 1 and Visualization State Reads Writes Moves Calls 0 0 1 L 13 2 1 1 R 3 2 0 0 R 2 3 0 0 L 4 3 1 1 R 3 4 1 0 R 5 5 0 1 L 6 5 1 1 R 5 6 0 1 L 7 6 1 1 L 6 7 0 0 L 11 7 1 0 R 5 9 0 0 R 12 9 9 1 0 R 10 10 0 0 R 2 10 1 1 R ...
work page 2016
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.