Busy beaver

InductiveHead movement#✓fully proved

A head movement is one of exactly two directions: left or right.

inductive Move where
  | left
  | right
deriving DecidableEq

Used by 15

Used byHead displacement bound · Busy Beaver score function · The Busy Beaver score is at most the shift · Busy Beaver shift function · Embedding a machine into one more state · The score function is attained · The shift function is attained · One-state machines halt within one step · Busy Beaver machine · Machine code · A one-state machine that stays in its state on a blank never halts · The number of ones grows by at most one per step · Head displacement · One step of a Busy Beaver machine · Cells far from the origin stay blank

DefinitionHead displacement#✓fully proved

The displacement of a head movement is \(-1\) for a move to the left and \(1\) for a move to the right.

def Move.shift : Move → ℤ
  | .left => -1
  | .right => 1

Uses 1 · Used by 6

Statement usesHead movement

Used byHead displacement bound · One-state machines halt within one step · A one-state machine that stays in its state on a blank never halts · The number of ones grows by at most one per step · One step of a Busy Beaver machine · Cells far from the origin stay blank

AbbreviationBusy Beaver machine#✓fully proved

A Busy Beaver machine with \(n\) working states is a transition table that assigns to each of the \(n\) working states and each read symbol in \(\{0, 1\}\) a symbol in \(\{0, 1\}\) to write, a head movement (left or right), and a next state, which is either one of the \(n\) working states or the halt state.

The write and move of a halting transition are still performed, and the halting step counts toward the runtime.

abbrev Machine (n : ℕ) :=
  Fin n → Fin 2 → Fin 2 × Move × Option (Fin n)

Uses 1 · Used by 30

Statement usesHead movement

Used byHead displacement bound · Busy Beaver score function · The Busy Beaver score is at most the shift · Busy Beaver shift function · Theories deciding halting at a state count · ZFC-like theories decide halting through five states · Decidability of halting passes to fewer states · Embedding a machine into one more state · The score function is attained · The shift function is attained · Halting time · Halting on the blank tape · Halting sentence of a machine · Halting within \(t\) steps · One-state machines halt within one step · Machine code · After \(t\) steps, every one lies within distance \(t\) of the origin · A consistency-search machine blocks decidability at its size · A one-state machine that stays in its state on a blank never halts · Non-halting sentence of a machine · Number of ones after \(t\) steps · At most \(t\) ones after \(t\) steps · The number of ones grows by at most one per step · Configuration after \(t\) steps · Score of a machine · Soundness for halting sentences · One step of a Busy Beaver machine · Runtime of a Busy Beaver machine · Cells far from the origin stay blank · Proof-checker presentation of a ZFC-like theory

StructureBusy Beaver machine configuration#✓fully proved

A configuration of an \(n\)-state machine consists of a current state, which is either one of the \(n\) working states or the halt state, an integer head position, and a tape assigning a symbol in \(\{0, 1\}\) to every integer cell.

structure Config (n : ℕ) where
  state : Option (Fin n)
  head : ℤ
  tape : ℤ → Fin 2

Used by 13

Used byHead displacement bound · Embedding a configuration into one more state · Halting within \(t\) steps · One-state machines halt within one step · Initial configuration of a Busy Beaver machine · After \(t\) steps, every one lies within distance \(t\) of the origin · A one-state machine that stays in its state on a blank never halts · Number of ones after \(t\) steps · At most \(t\) ones after \(t\) steps · The number of ones grows by at most one per step · Configuration after \(t\) steps · One step of a Busy Beaver machine · Cells far from the origin stay blank

DefinitionOne step of a Busy Beaver machine#✓fully proved

Let \(M\) be a machine with \(n\) working states and let \(c\) be a configuration with head position \(h\). If \(c\) is halted, the step leaves \(c\) unchanged. Otherwise let \(q\) be the current state, let \(a\) be the symbol in cell \(h\), and let \(M(q, a) = (b, d, q')\). The step writes \(b\) in cell \(h\), leaving every other cell unchanged, moves the head to \(h - 1\) if \(d\) is left and to \(h + 1\) if \(d\) is right, and passes to the state \(q'\), which may be the halt state.

def step {n : ℕ} (M : Machine n) (c : Config n) : Config n :=
  match c.state with
  | none => c
  | some q =>
    let a := M q (c.tape c.head)
    ⟨a.2.2, c.head + a.2.1.shift, Function.update c.tape c.head a.1⟩

Uses 4 · Used by 6

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Head movement · Head displacement

Used byHead displacement bound · One-state machines halt within one step · A one-state machine that stays in its state on a blank never halts · The number of ones grows by at most one per step · Configuration after \(t\) steps · Cells far from the origin stay blank

DefinitionInitial state#✓fully proved

For a machine with \(n\) working states, the initial state is state \(0\) when \(n > 0\), and the halt state when \(n = 0\).

def initialState (n : ℕ) : Option (Fin n) :=
  if h : 0 < n then some ⟨0, h⟩ else none

Used by 3

Used byOne-state machines halt within one step · Initial configuration of a Busy Beaver machine · A one-state machine that stays in its state on a blank never halts

DefinitionInitial configuration of a Busy Beaver machine#✓fully proved

The initial configuration of a machine with \(n\) working states is in the initial state (state \(0\), or the halt state when \(n = 0\)), with the head at position \(0\) and every tape cell blank, that is, holding the symbol \(0\).

def initial (n : ℕ) : Config n :=
  ⟨initialState n, 0, fun _ => 0⟩

Uses 2 · Used by 6

Statement usesBusy Beaver machine configuration · Initial state

Used byHead displacement bound · One-state machines halt within one step · A one-state machine that stays in its state on a blank never halts · The number of ones grows by at most one per step · Configuration after \(t\) steps · Cells far from the origin stay blank

DefinitionConfiguration after \(t\) steps#✓fully proved

For a Busy Beaver machine \(M\) and \(t \in \mathbb{N}\), the configuration of \(M\) after \(t\) steps is the result of applying the one-step map of \(M\) \(t\) times to the initial configuration on the blank tape.

def run {n : ℕ} (M : Machine n) (t : ℕ) : Config n :=
  (step M)^[t] (initial n)

Uses 4 · Used by 9

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Initial configuration of a Busy Beaver machine · One step of a Busy Beaver machine

Used byHead displacement bound · Halting within \(t\) steps · One-state machines halt within one step · After \(t\) steps, every one lies within distance \(t\) of the origin · A one-state machine that stays in its state on a blank never halts · Number of ones after \(t\) steps · At most \(t\) ones after \(t\) steps · The number of ones grows by at most one per step · Cells far from the origin stay blank

DefinitionHalting within \(t\) steps#✓fully proved

A Busy Beaver machine \(M\) with \(n\) working states halts within \(t\) steps when the configuration reached after running \(M\) for \(t\) steps from the initial blank-tape configuration is in the halt state.

def HaltsWithin {n : ℕ} (M : Machine n) (t : ℕ) : Prop :=
  (run M t).state = none

Uses 3 · Used by 6

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Configuration after \(t\) steps

Used byZFC-like theories decide halting through five states · Halting time · Halting on the blank tape · One-state machines halt within one step · A one-state machine that stays in its state on a blank never halts · Proof-checker presentation of a ZFC-like theory

DefinitionHalting on the blank tape#✓fully proved

A Busy Beaver machine \(M\) halts when there is a number of steps \(t\) such that \(M\) halts within \(t\) steps, that is, when \(M\) started from the initial blank-tape configuration eventually reaches the halt state.

def Halts {n : ℕ} (M : Machine n) : Prop :=
  ∃ t, HaltsWithin M t

Uses 2 · Used by 9

Statement usesHalting within \(t\) steps · Busy Beaver machine

Used byThe Busy Beaver score is at most the shift · Halting time · One-state machines halt within one step · A consistency-search machine blocks decidability at its size · A one-state machine that stays in its state on a blank never halts · Score of a machine · Soundness for halting sentences · Runtime of a Busy Beaver machine · Proof-checker presentation of a ZFC-like theory

DefinitionHalting time#✓fully proved

For an \(n\)-state machine \(M\) that halts on the blank tape, its halting time is the least \(t\) such that \(M\), started on the blank tape, is in the halt state after \(t\) steps.

noncomputable def haltTime {n : ℕ} (M : Machine n) (h : Halts M) : ℕ :=
  @Nat.find _ (fun t => Classical.propDecidable _) h

Uses 3 · Used by 3

Statement usesHalting on the blank tape · Halting within \(t\) steps · Busy Beaver machine

Used byThe Busy Beaver score is at most the shift · Score of a machine · Runtime of a Busy Beaver machine

TheoremHead displacement bound#✓fully proved

For every \(n\)-state Busy Beaver machine \(M\) and every \(t \in \mathbb{N}\), if \(h \in \mathbb{Z}\) is the head position after \(M\) has run for \(t\) steps from the initial configuration on the blank tape, then \(|h| \le t\).

theorem abs_head_le {n : ℕ} (M : Machine n) (t : ℕ) :
    |(run M t).head| ≤ t

Uses 7 · Used by 1

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Configuration after \(t\) steps

Proof usesHead movement · Head displacement · Initial configuration of a Busy Beaver machine · One step of a Busy Beaver machine

Used byCells far from the origin stay blank

TheoremCells far from the origin stay blank#✓fully proved

Let \(M\) be a machine with \(n\) working states, started in cell \(0\) on the blank tape. For every \(t \in \mathbb{N}\) and every cell \(i \in \mathbb{Z}\) with \(|i| > t\), the symbol in cell \(i\) after \(t\) steps is \(0\).

theorem tape_eq_zero_of_abs_gt {n : ℕ} (M : Machine n) (t : ℕ)
    {i : ℤ} (hi : t < |i|) : (run M t).tape i = 0

Uses 8 · Used by 2

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Configuration after \(t\) steps

Proof usesHead movement · Head displacement · Head displacement bound · Initial configuration of a Busy Beaver machine · One step of a Busy Beaver machine

Used byAfter \(t\) steps, every one lies within distance \(t\) of the origin · A one-state machine that stays in its state on a blank never halts

DefinitionNumber of ones after \(t\) steps#✓fully proved

For a Busy Beaver machine \(M\) and \(t \in \mathbb{N}\), the number of ones of \(M\) after \(t\) steps is the number of cells \(i \in \mathbb{Z}\) with \(-t \le i \le t\) that hold the symbol \(1\) in the configuration of \(M\) after \(t\) steps, started on the blank tape.

Every one on the tape after \(t\) steps lies in this window, since the head moves at most one cell per step.

def onesAt {n : ℕ} (M : Machine n) (t : ℕ) : ℕ :=
  ((Finset.Icc (-(t : ℤ)) t).filter fun i => (run M t).tape i = 1).card

Uses 3 · Used by 4

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Configuration after \(t\) steps

Used byThe Busy Beaver score is at most the shift · At most \(t\) ones after \(t\) steps · The number of ones grows by at most one per step · Score of a machine

TheoremAfter \(t\) steps, every one lies within distance \(t\) of the origin#✓fully proved

For every Busy Beaver machine \(M\), every \(t \in \mathbb{N}\) and every cell \(i \in \mathbb{Z}\), if cell \(i\) holds the symbol \(1\) after \(M\) runs for \(t\) steps from the initial blank-tape configuration, then \(-t \le i \le t\).

theorem mem_window_of_tape_eq_one {n : ℕ} (M : Machine n) (t : ℕ) {i : ℤ}
    (hi : (run M t).tape i = 1) : i ∈ Finset.Icc (-(t : ℤ)) t

Uses 4 · Used by 1

Statement usesBusy Beaver machine configuration · Busy Beaver machine · Configuration after \(t\) steps

Proof usesCells far from the origin stay blank

Used byThe number of ones grows by at most one per step

TheoremThe number of ones grows by at most one per step#✓fully proved

For every Busy Beaver machine \(M\) and every \(t \in \mathbb{N}\), the number of ones of \(M\) after \(t + 1\) steps is at most the number of ones of \(M\) after \(t\) steps plus \(1\).

theorem onesAt_succ_le {n : ℕ} (M : Machine n) (t : ℕ) :
    onesAt M (t + 1) ≤ onesAt M t + 1

Uses 9 · Used by 1

Statement usesBusy Beaver machine · Number of ones after \(t\) steps

Proof usesBusy Beaver machine configuration · Head movement · Head displacement · Initial configuration of a Busy Beaver machine · After \(t\) steps, every one lies within distance \(t\) of the origin · Configuration after \(t\) steps · One step of a Busy Beaver machine

Used byAt most \(t\) ones after \(t\) steps

TheoremAt most \(t\) ones after \(t\) steps#✓fully proved

For every Busy Beaver machine \(M\) and every \(t \in \mathbb{N}\), the number of ones of \(M\) after \(t\) steps is at most \(t\).

theorem onesAt_le_steps {n : ℕ} (M : Machine n) (t : ℕ) :
    onesAt M t ≤ t

Uses 5 · Used by 1

Statement usesBusy Beaver machine · Number of ones after \(t\) steps

Proof usesBusy Beaver machine configuration · The number of ones grows by at most one per step · Configuration after \(t\) steps

Used byThe Busy Beaver score is at most the shift

DefinitionRuntime of a Busy Beaver machine#✓fully proved

For a machine \(M\) with \(n\) working states, the runtime of \(M\) is its halting time on the blank tape if \(M\) halts, and \(0\) if \(M\) does not halt. This is the quantity whose maximum over all \(n\)-state machines is the shift function \(S(n)\).

noncomputable def stepsOf {n : ℕ} (M : Machine n) : ℕ :=
  @dite ℕ (Halts M) (Classical.propDecidable _) (fun h => haltTime M h)
    (fun _ => 0)

Uses 3 · Used by 3

Statement usesHalting on the blank tape · Busy Beaver machine · Halting time

Used byThe Busy Beaver score is at most the shift · Busy Beaver shift function · The shift function is attained

DefinitionScore of a machine#✓fully proved

For a Busy Beaver machine \(M\): if \(M\) halts on the blank tape, with halting time \(T\), its score is the number of ones of \(M\) after \(T\) steps; if \(M\) does not halt, its score is \(0\).

noncomputable def scoreOf {n : ℕ} (M : Machine n) : ℕ :=
  @dite ℕ (Halts M) (Classical.propDecidable _)
    (fun h => onesAt M (haltTime M h)) (fun _ => 0)

Uses 4 · Used by 3

Statement usesHalting on the blank tape · Busy Beaver machine · Halting time · Number of ones after \(t\) steps

Used byBusy Beaver score function · The Busy Beaver score is at most the shift · The score function is attained

DefinitionBusy Beaver shift function#✓fully proved

For \(n \in \mathbb{N}\), Rado's shift function \(S(n)\) is the largest halting time of an \(n\)-state two-symbol machine that halts when started on the blank tape; machines that do not halt contribute \(0\).

noncomputable def busyBeaverSteps (n : ℕ) : ℕ :=
  (Finset.univ : Finset (Machine n)).sup stepsOf

Uses 3 · Used by 7

Statement usesBusy Beaver machine · Head movement · Runtime of a Busy Beaver machine

Used byThe Busy Beaver score is at most the shift · Five-state Busy Beaver shift value · Four-state Busy Beaver shift value · Three-state Busy Beaver shift value · ZFC-like theories decide halting through five states · The shift function is attained · Proof-checker presentation of a ZFC-like theory

DefinitionBusy Beaver score function#✓fully proved

For \(n \in \mathbb{N}\), Rado's score function \(\Sigma(n)\) is the largest number of ones left on the tape, at its halting time, by an \(n\)-state two-symbol machine that halts when started on the blank tape; machines that do not halt contribute \(0\).

noncomputable def busyBeaverOnes (n : ℕ) : ℕ :=
  (Finset.univ : Finset (Machine n)).sup scoreOf

Uses 3 · Used by 5

Statement usesBusy Beaver machine · Head movement · Score of a machine

Used byFive-state Busy Beaver score value · Four-state Busy Beaver score value · The Busy Beaver score is at most the shift · Three-state Busy Beaver score value · The score function is attained

TheoremThe Busy Beaver score is at most the shift#✓fully proved

For every \(n \in \mathbb{N}\), Rado's score function \(\Sigma\) and Rado's shift function \(S\) satisfy \(\Sigma(n) \le S(n)\): the largest number of ones left on the tape by a halting \(n\)-state two-symbol machine started on the blank tape is at most the largest halting time of such a machine.

theorem busyBeaverOnes_le_steps (n : ℕ) :
    busyBeaverOnes n ≤ busyBeaverSteps n

Uses 10

Statement usesBusy Beaver score function · Busy Beaver shift function

Proof usesHalting on the blank tape · Busy Beaver machine · Head movement · Halting time · Number of ones after \(t\) steps · At most \(t\) ones after \(t\) steps · Score of a machine · Runtime of a Busy Beaver machine

TheoremThe shift function is attained#✓fully proved

Let \(S(n)\) be Rado's shift function, the largest runtime of an \(n\)-state machine, where the runtime of a machine is its halting time on the blank tape if it halts and \(0\) otherwise. For every \(n\), some \(n\)-state machine \(M\) has runtime equal to \(S(n)\). Thus \(S(n)\) is the halting time of a halting \(n\)-state machine, or \(S(n) = 0\).

theorem exists_stepsOf_eq (n : ℕ) :
    ∃ M : Machine n, stepsOf M = busyBeaverSteps n

Uses 4

Statement usesBusy Beaver machine · Busy Beaver shift function · Runtime of a Busy Beaver machine

Proof usesHead movement

TheoremThe score function is attained#✓fully proved

Let \(\Sigma(n)\) be the busy beaver score function, the largest score of an \(n\)-state machine, where the score of a machine is the number of ones on its final tape if it halts on the blank tape and \(0\) otherwise. For every \(n\), some \(n\)-state machine \(M\) has score equal to \(\Sigma(n)\). Thus \(\Sigma(n)\) is the number of ones left by a halting \(n\)-state machine, or \(\Sigma(n) = 0\).

theorem exists_scoreOf_eq (n : ℕ) :
    ∃ M : Machine n, scoreOf M = busyBeaverOnes n

Uses 4

Statement usesBusy Beaver machine · Busy Beaver score function · Score of a machine

Proof usesHead movement

DefinitionEmbedding a machine into one more state#✓fully proved

An \(n\)-state machine \(M\) is embedded into \(n + 1\) states as follows. In a working state \(q < n\) reading a symbol \(s\), the new machine writes the symbol, makes the move and enters the next state that \(M\) prescribes in state \(q\) on \(s\), halting when \(M\) halts. In the new state \(n\) it writes \(0\), moves left and halts, whatever it reads.

No transition enters state \(n\). So for \(n \ge 1\), where the machine starts in state \(0 < n\), the new state is never reached; for \(n = 0\) the new state is the start state.

def embedMachine {n : ℕ} (M : Machine n) : Machine (n + 1) :=
  fun q s =>
    if h : q.val < n then
      let a := M ⟨q.val, h⟩ s
      (a.1, a.2.1, a.2.2.map Fin.castSucc)
    else (0, Move.left, none)

Uses 2 · Used by 1

Statement usesBusy Beaver machine · Head movement

Used byDecidability of halting passes to fewer states

DefinitionEmbedding a configuration into one more state#✓fully proved

For a configuration \(c\) of an \(n\)-state machine, its embedding is the configuration for \(n + 1\) states with the same head position and the same tape as \(c\). Its state is the state of \(c\), where a working state \(q \in \{0, \dots, n - 1\}\) stays \(q\) and the halt state stays the halt state.

def embedConfig {n : ℕ} (c : Config n) : Config (n + 1) :=
  ⟨c.state.map Fin.castSucc, c.head, c.tape⟩

Uses 1

Statement usesBusy Beaver machine configuration

TheoremA one-state machine that stays in its state on a blank never halts#✓fully proved

Let \(M\) be a Busy Beaver machine with a single working state \(0\). If the transition of \(M\) from state \(0\) on reading the blank symbol \(0\) has next state \(0\), then \(M\) does not halt.

Such a machine marches in one direction forever: at every step the head is on a previously unvisited blank cell.

theorem not_halts_of_one_state_march (M : Machine 1)
    (hnext : (M 0 0).2.2 = some 0) : ¬ Halts M

Uses 11 · Used by 1

Statement usesHalting on the blank tape · Busy Beaver machine · Head movement

Proof usesBusy Beaver machine configuration · Halting within \(t\) steps · Head displacement · Initial configuration of a Busy Beaver machine · Initial state · Configuration after \(t\) steps · One step of a Busy Beaver machine · Cells far from the origin stay blank

Used byOne-state machines halt within one step

TheoremOne-state machines halt within one step#✓fully proved

Every halting one-state machine halts within one step.

theorem haltsWithin_one_of_halts (M : Machine 1) (h : Halts M) :
    HaltsWithin M 1

Uses 11

Statement usesHalting on the blank tape · Halting within \(t\) steps · Busy Beaver machine

Proof usesBusy Beaver machine configuration · Head movement · Head displacement · Initial configuration of a Busy Beaver machine · Initial state · A one-state machine that stays in its state on a blank never halts · Configuration after \(t\) steps · One step of a Busy Beaver machine

DefinitionMachine code#✓fully proved

The code of a machine \(M\) with \(n\) working states is the natural number that encodes the pair \((n, i)\) under a fixed pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\), where \(i\) is the index of \(M\) in a fixed enumeration of the finitely many machines with \(n\) working states.

noncomputable def machineCode {n : ℕ} (M : Machine n) : ℕ :=
  Nat.pair n (Fintype.equivFinOfCardEq (α := Machine n) rfl M).val

Uses 2 · Used by 2

Statement usesBusy Beaver machine · Head movement

Used byHalting sentence of a machine · Non-halting sentence of a machine

DefinitionSentence codes#✓fully proved

The sentence code with tag \(a\) and payload \(p\) is the natural number \(4p + a\). The tags in use are \(0\) (the coded machine halts), \(1\) (the coded machine does not halt), \(2\) (the false sentence), and \(3\) with payload the pairing code of \(n\) and \(B\) (every halting \(n\)-state machine halts within \(B\) steps).

Sentences are natural numbers rather than propositions, so provability does not collapse under propositional extensionality.

def sentenceCode (tag payload : ℕ) : ℕ :=
  4 * payload + tag

Used by 4

Used byRuntime-bound sentence · The false sentence · Halting sentence of a machine · Non-halting sentence of a machine

DefinitionHalting sentence of a machine#✓fully proved

For an \(n\)-state machine \(M\), the halting sentence of \(M\) is the sentence code with tag \(0\) and payload the code of \(M\). It stands for "\(M\) halts on the blank tape"; this meaning comes from soundness hypotheses on a theory, not from the code itself.

noncomputable def haltsSentence {n : ℕ} (M : Machine n) : ℕ :=
  sentenceCode 0 (machineCode M)

Uses 3 · Used by 6

Statement usesBusy Beaver machine · Machine code · Sentence codes

Used byTheories deciding halting at a state count · ZFC-like theories decide halting through five states · Decidability of halting passes to fewer states · A consistency-search machine blocks decidability at its size · Soundness for halting sentences · Proof-checker presentation of a ZFC-like theory

DefinitionNon-halting sentence of a machine#✓fully proved

For a Busy Beaver machine \(M\), the non-halting sentence of \(M\) is the sentence code with tag \(1\) whose payload is the code of \(M\); it stands for "\(M\) does not halt on the blank tape".

noncomputable def notHaltsSentence {n : ℕ} (M : Machine n) : ℕ :=
  sentenceCode 1 (machineCode M)

Uses 3 · Used by 6

Statement usesBusy Beaver machine · Machine code · Sentence codes

Used byTheories deciding halting at a state count · ZFC-like theories decide halting through five states · Decidability of halting passes to fewer states · A consistency-search machine blocks decidability at its size · Soundness for halting sentences · Proof-checker presentation of a ZFC-like theory

DefinitionThe false sentence#✓fully proved

The false sentence is the sentence code with tag \(2\) and payload \(0\), that is, the natural number \(2\).

def falseSentence : ℕ :=
  sentenceCode 2 0

Uses 1 · Used by 2

Statement usesSentence codes

Used byConsistent formal theory · A consistency-search machine blocks decidability at its size

DefinitionRuntime-bound sentence#✓fully proved

For natural numbers \(n\) and \(B\), the runtime-bound sentence is the sentence code with tag \(3\) and payload \(\langle n, B \rangle\), the pairing of \(n\) and \(B\); as a number it equals \(4 \langle n, B \rangle + 3\).

Its intended reading is "every halting \(n\)-state machine halts within \(B\) steps"; this meaning is assigned only through separate soundness hypotheses.

def boundSentence (n B : ℕ) : ℕ :=
  sentenceCode 3 (Nat.pair n B)

Uses 1 · Used by 2

Statement usesSentence codes

Used byZFC-like theories decide halting through five states · Proof-checker presentation of a ZFC-like theory

StructureFormal theory#✓fully proved

A formal theory is given by a provability predicate on sentence codes, which are natural numbers: for each natural number it specifies whether that sentence code is provable in the theory.

The theory is an abstract parameter, with ZFC as the intended instance. No meaning is attached to sentence codes here; the halting, non-halting, false and runtime-bound sentences receive their meaning through separate soundness hypotheses.

structure FormalTheory where
  /-- Provability of a sentence code in the theory. -/
  Provable : ℕ → Prop

Used by 9

Used byConsistent formal theory · Theories deciding halting at a state count · ZFC-like theories decide halting through five states · Decidability of halting passes to fewer states · First undecidable number of states · A consistency-search machine blocks decidability at its size · Decidability through five states and the first undecidable size · Soundness for halting sentences · Proof-checker presentation of a ZFC-like theory

DefinitionConsistent formal theory#✓fully proved

A formal theory \(T\) is consistent when \(T\) does not prove the false sentence.

def Consistent (T : FormalTheory) : Prop :=
  ¬ T.Provable falseSentence

Uses 2 · Used by 1

Statement usesFormal theory · The false sentence

Used byA consistency-search machine blocks decidability at its size

DefinitionSoundness for halting sentences#✓fully proved

A formal theory \(T\) is sound for halting sentences when, for every \(n\) and every Busy Beaver machine \(M\) with \(n\) states, if \(T\) proves the halting sentence of \(M\) then \(M\) halts on the blank tape, and if \(T\) proves the non-halting sentence of \(M\) then \(M\) does not halt on the blank tape.

def SoundForHalting (T : FormalTheory) : Prop :=
  (∀ {n : ℕ} (M : Machine n), T.Provable (haltsSentence M) → Halts M) ∧
  (∀ {n : ℕ} (M : Machine n),
    T.Provable (notHaltsSentence M) → ¬ Halts M)

Uses 5 · Used by 1

Statement usesFormal theory · Halting on the blank tape · Busy Beaver machine · Halting sentence of a machine · Non-halting sentence of a machine

Used byProof-checker presentation of a ZFC-like theory

DefinitionTheories deciding halting at a state count#✓fully proved

A formal theory \(T\) decides halting for \(n\)-state machines when, for every \(n\)-state machine \(M\), \(T\) proves the halting sentence of \(M\) or \(T\) proves the non-halting sentence of \(M\).

def DecidesHalting (T : FormalTheory) (n : ℕ) : Prop :=
  ∀ M : Machine n,
    T.Provable (haltsSentence M) ∨ T.Provable (notHaltsSentence M)

Uses 4 · Used by 5

Statement usesFormal theory · Busy Beaver machine · Halting sentence of a machine · Non-halting sentence of a machine

Used byZFC-like theories decide halting through five states · Decidability of halting passes to fewer states · First undecidable number of states · A consistency-search machine blocks decidability at its size · Decidability through five states and the first undecidable size

DefinitionFirst undecidable number of states#✓fully proved

For a formal theory \(T\), the first undecidable number of states is the least \(n\) such that \(T\) does not decide halting for all \(n\)-state machines, that is, there is an \(n\)-state machine \(M\) for which \(T\) proves neither the halting sentence nor the non-halting sentence of \(M\). It is \(0\) when there is no such \(n\).

For ZFC this is catalogue constant 14a; the junk value \(0\) covers a theory that decides halting at every number of states.

noncomputable def firstUndecidable (T : FormalTheory) : ℕ :=
  sInf {n | ¬ DecidesHalting T n}

Uses 2 · Used by 1

Statement usesTheories deciding halting at a state count · Formal theory

Used byDecidability through five states and the first undecidable size

TheoremDecidability through five states and the first undecidable size#✓fully proved

If a formal theory \(T\) decides halting for \(n\)-state machines for every \(n \le 5\), and fails to decide halting for \(n\)-state machines for some \(n\), then the first undecidable size of \(T\) is at least \(6\).

This is the shape of the catalogue lower bound from the determination of the five-state Busy Beaver value.

theorem six_le_firstUndecidable_of_decides_le_five {T : FormalTheory}
    (h5 : ∀ n ≤ 5, DecidesHalting T n)
    (hex : ∃ n, ¬ DecidesHalting T n) :
    6 ≤ firstUndecidable T

Uses 3

Statement usesTheories deciding halting at a state count · Formal theory · First undecidable number of states

TheoremA consistency-search machine blocks decidability at its size#✓fully proved

Let \(T\) be a formal theory and \(M\) a Busy Beaver machine with \(n\) working states. Suppose that \(M\) halts if and only if \(T\) proves the false sentence, that \(M\) halts whenever \(T\) proves the halting sentence of \(M\), that \(T\) is consistent, and that \(T\) does not prove the non-halting sentence of \(M\). Then \(T\) does not decide halting for all machines with \(n\) working states.

The last hypothesis is the Gödel second-incompleteness content when \(T\) is ZFC.

theorem not_decides_of_consistency_machine {T : FormalTheory} {n : ℕ}
    (M : Machine n) (hM : Halts M ↔ T.Provable falseSentence)
    (hsound : T.Provable (haltsSentence M) → Halts M)
    (hcons : Consistent T)
    (hnot : ¬ T.Provable (notHaltsSentence M)) :
    ¬ DecidesHalting T n

Uses 8

Statement usesConsistent formal theory · Theories deciding halting at a state count · Formal theory · Halting on the blank tape · Busy Beaver machine · The false sentence · Halting sentence of a machine · Non-halting sentence of a machine

TheoremDecidability of halting passes to fewer states#✓fully proved

Let \(T\) be a formal theory such that, for every \(m\) and every Busy Beaver machine \(M\) with \(m\) working states, if \(T\) proves the halting sentence of the embedding of \(M\) into \(m + 1\) states then \(T\) proves the halting sentence of \(M\), and if \(T\) proves the non-halting sentence of the embedding of \(M\) into \(m + 1\) states then \(T\) proves the non-halting sentence of \(M\). Then for every \(n\), if \(T\) decides halting for machines with \(n + 1\) working states, it decides halting for machines with \(n\) working states.

The transport hypotheses are where a real theory would rewrite a proof about the embedded machine into a proof about the original machine; they are stated explicitly because provability of one sentence code does not formally imply provability of another.

theorem decidesHalting_of_succ {T : FormalTheory}
    (htransport : ∀ {n : ℕ} (M : Machine n),
      (T.Provable (haltsSentence (embedMachine M)) →
        T.Provable (haltsSentence M)) ∧
      (T.Provable (notHaltsSentence (embedMachine M)) →
        T.Provable (notHaltsSentence M)))
    {n : ℕ} (h : DecidesHalting T (n + 1)) :
    DecidesHalting T n

Uses 6

Statement usesTheories deciding halting at a state count · Formal theory · Busy Beaver machine · Embedding a machine into one more state · Halting sentence of a machine · Non-halting sentence of a machine

StructureProof-checker presentation of a ZFC-like theory#✓fully proved

A ZFC-like presentation consists of a formal theory \(T\), given by a provability predicate on sentence codes in \(\mathbb{N}\), together with a Boolean proof checker \(\mathrm{check}(p, s)\) on pairs of natural numbers, such that the following hold. A sentence code \(s\) is provable in \(T\) if and only if \(\mathrm{check}(p, s)\) is true for some \(p \in \mathbb{N}\). \(T\) is sound for halting: for every machine \(M\), if \(T\) proves the halting sentence of \(M\) then \(M\) halts on the blank tape, and if \(T\) proves the non-halting sentence of \(M\) then \(M\) does not halt. For every machine \(M\), if \(M\) has halted within \(t\) steps for some \(t\), then \(T\) proves the halting sentence of \(M\). Write \(S(n)\) for the Busy Beaver shift function, the largest halting time of a halting machine with \(n\) working states, and call the bound sentence for \(n\) and \(B\) the sentence code saying that every halting machine with \(n\) working states halts within \(B\) steps. For every \(n \le 5\), \(T\) proves the bound sentence for \(n\) and \(S(n)\). Whenever \(T\) proves the bound sentence for \(n\) and \(B\), every halting machine with \(n\) working states halts within \(B\) steps. Whenever \(T\) proves the bound sentence for \(n\) and \(B\) and a machine \(M\) with \(n\) working states has not halted within \(B\) steps, \(T\) proves the non-halting sentence of \(M\).

No concrete syntax or proof checker for ZFC is given, and no presentation of ZFC is constructed; the intended instance is ZFC with its standard proof checker. The state counts for consistency-search machines in the literature depend on specific checker implementations and are not asserted for arbitrary presentations.

Cslib.BusyBeaver.ZFCPresentation · 28 lines

structure ZFCPresentation where
  /-- The presented theory. -/
  theory : FormalTheory
  /-- The proof checker: `check p s` says `p` proves sentence `s`. -/
  check : ℕ → ℕ → Bool
  /-- Provability is existence of a checked proof. -/
  provable_iff : ∀ s : ℕ,
    theory.Provable s ↔ ∃ p : ℕ, check p s = true
  /-- Soundness for halting sentences. -/
  soundForHalting : SoundForHalting theory
  /-- Finite halting computations are verifiable. -/
  verifies_halting : ∀ {n : ℕ} (M : Machine n) (t : ℕ),
    HaltsWithin M t → theory.Provable (haltsSentence M)
  /-- The computed Busy Beaver bounds through five states are
  provable. -/
  verifies_bounds : ∀ n ≤ 5,
    theory.Provable (boundSentence n (busyBeaverSteps n))
  /-- A proved runtime bound applies to the machines it quantifies
  over. -/
  sound_bounds : ∀ (n B : ℕ),
    theory.Provable (boundSentence n B) →
      ∀ M : Machine n, Halts M → HaltsWithin M B
  /-- A proved runtime bound together with a finite non-halting run
  yields a proof of the non-halting sentence. This packages finite
  run verification and modus ponens inside the theory. -/
  notHalts_of_bound : ∀ {n : ℕ} (M : Machine n) (B : ℕ),
    theory.Provable (boundSentence n B) → ¬ HaltsWithin M B →
      theory.Provable (notHaltsSentence M)

Uses 9 · Used by 1

Statement usesFormal theory · Halting on the blank tape · Halting within \(t\) steps · Busy Beaver machine · Soundness for halting sentences · Runtime-bound sentence · Busy Beaver shift function · Halting sentence of a machine · Non-halting sentence of a machine

Used byZFC-like theories decide halting through five states

TheoremZFC-like theories decide halting through five states#✓fully proved

For every ZFC-like presentation \(Z\) and every \(n \le 5\), the theory presented by \(Z\) decides halting for \(n\)-state machines: for every \(n\)-state machine it proves the machine's halting sentence or its non-halting sentence.

Proof idea: let \(S\) be Rado's shift function; \(Z\) proves the runtime bound \(S(n)\) for halting \(n\)-state machines. Run each machine for \(S(n)\) steps; if it has halted, the computation verifies, and if it has not, the bound derives its non-halting sentence.

theorem ZFCPresentation.decidesHalting_le_five (Z : ZFCPresentation) :
    ∀ n ≤ 5, DecidesHalting Z.theory n

Uses 9

Statement usesTheories deciding halting at a state count · Formal theory · Proof-checker presentation of a ZFC-like theory

Proof usesHalting within \(t\) steps · Busy Beaver machine · Runtime-bound sentence · Busy Beaver shift function · Halting sentence of a machine · Non-halting sentence of a machine

TheoremThree-state Busy Beaver shift value#●ready to prove

Rado's shift function \(S\) satisfies \(S(3) = 21\): among the two-symbol Busy Beaver machines with \(3\) working states that halt when started on the blank tape, the largest halting time is \(21\).

theorem_wanted busyBeaverSteps_three_wanted :
    busyBeaverSteps 3 = 21

Sources

• Lin--Radó (1965), determination of S(3) = 21.

Uses 1

Statement usesBusy Beaver shift function

TheoremThree-state Busy Beaver score value#●ready to prove

Rado's score function \(\Sigma\) satisfies \(\Sigma(3) = 6\): among the two-symbol Busy Beaver machines with \(3\) working states that halt when started on the blank tape, the largest number of ones left on the tape at the halting time is \(6\).

theorem_wanted busyBeaverOnes_three_wanted :
    busyBeaverOnes 3 = 6

Sources

• Lin--Radó (1965), determination of Σ(3) = 6.

Uses 1

Statement usesBusy Beaver score function

TheoremFour-state Busy Beaver shift value#●ready to prove

Rado's shift function \(S\) satisfies \(S(4) = 107\): among the two-symbol Busy Beaver machines with \(4\) working states that halt when started on the blank tape, the largest halting time is \(107\).

theorem_wanted busyBeaverSteps_four_wanted :
    busyBeaverSteps 4 = 107

Sources

• Brady (1983), determination of S(4) = 107.

Uses 1

Statement usesBusy Beaver shift function

TheoremFour-state Busy Beaver score value#●ready to prove

Rado's score function \(\Sigma\) satisfies \(\Sigma(4) = 13\): among the two-symbol Busy Beaver machines with \(4\) working states that halt when started on the blank tape, the largest number of ones left on the tape at the halting time is \(13\).

theorem_wanted busyBeaverOnes_four_wanted :
    busyBeaverOnes 4 = 13

Sources

• Brady (1983), determination of Σ(4) = 13.

Uses 1

Statement usesBusy Beaver score function

TheoremFive-state Busy Beaver shift value#●ready to prove

Rado's shift function \(S\) satisfies \(S(5) = 47176870\): among the two-symbol Busy Beaver machines with \(5\) working states that halt when started on the blank tape, the largest halting time is \(47176870\).

theorem_wanted busyBeaverSteps_five_wanted :
    busyBeaverSteps 5 = 47176870

Sources

• Busy Beaver Challenge (2025), determination of S(5) = 47176870.

Uses 1

Statement usesBusy Beaver shift function

TheoremFive-state Busy Beaver score value#●ready to prove

Rado's score function \(\Sigma\) satisfies \(\Sigma(5) = 4098\): among the two-symbol Busy Beaver machines with \(5\) working states that halt when started on the blank tape, the largest number of ones left on the tape at the halting time is \(4098\).

theorem_wanted busyBeaverOnes_five_wanted :
    busyBeaverOnes 5 = 4098

Sources

• Busy Beaver Challenge (2025), determination of Σ(5) = 4098.

Uses 1

Statement usesBusy Beaver score function

44 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.