BusyBeavers.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

25 declarations, 0 contain sorry, 0 declared as axioms

Turing Machines, Busy Beaver version.

A variant on the definition of the TM0 model in Mathlib: while the statements the TM can make in the usual TM0 are split into two categories (either write at the current position or move left/right), we want to combine the two to stick to the BB convention: first write at the current position and then move left/right.

Note that this Turing Machine model also works with states of type Option Γ. This is because in the busy beaver context, the turing machines also have an addition "halting" state

See also https://git.sr.ht/~vigoux/busybeaver for a different approach to formalising these objects.

Imports (3)

Imported by 2 files

structure Turing.BusyBeaver.Stmt A Turing machine "statement" is just a command to write a symbol on the tape (at the current position) and then move left or right line 56 source
Source documentation
A Turing machine "statement" is just a command to write a symbol on the tape (at the current position) and then move left or right.

no axioms what this means
```
structure Stmt where write ::
…
```
def Turing.BusyBeaver.Machine Documented declaration: Machine line 75 source
Source documentation
A Post-Turing machine with symbol type Γ and label type Λ is a function which, given the current state q : Λ and the tape head a : Γ, either halts (returns none) or returns a new state q' : Option Λ and a Stmt describing what to do: a command to write a symbol and move left or right. Notice that there are two ways of halting at a given (state, head) pair: either the machine halts immediately (i.e. the function returns none), or the machine moves to the "halting state", i.e. none : Option Λ and performs one last action.
Typically, both Λ and Γ are required to be inhabited; the default value for Γ is the "blank" tape value, and the default value of Λ is the initial state.

no axioms what this means
Statement uses: Inhabited
Proof uses: Option, Prod, Turing.BusyBeaver.Stmt
```
def Machine [Inhabited Λ] :=
…
```
instance Turing.BusyBeaver.Machine.inhabited line 78 source
no axioms what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine
Proof uses: id, inferInstance, Option, Prod, Turing.BusyBeaver.Stmt
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
structure Turing.BusyBeaver.Cfg The configuration state of a Turing machine during operation consists of a label (machine state), and a tape line 88 source
Source documentation
The configuration state of a Turing machine during operation consists of a label (machine state), and a tape. The tape is represented in the form (a, L, R), meaning the tape looks like L.rev ++ [a] ++ R with the machine currently reading the a. The lists are automatically extended with blanks as the machine moves around.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited
```
structure Cfg [Inhabited Γ] where
…
```
instance Turing.BusyBeaver.Cfg.inhabited line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Cfg
Proof uses: Inhabited.mk, Turing.BusyBeaver.Cfg.mk, Inhabited.default, Option, Turing.Tape
2 instances, coercions and auxiliary constants left out.
def Turing.BusyBeaver.Machine.step Execution semantics of the Turing machine line 104 source
Source documentation
Execution semantics of the Turing machine.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Option
Proof uses: Turing.BusyBeaver.Machine.step.match_3, Turing.Tape, Option.none, Option.map, Prod, Turing.BusyBeaver.Stmt, Turing.BusyBeaver.Machine.step.match_2, Turing.BusyBeaver.Cfg.mk, Turing.BusyBeaver.Machine.step.match_1, Turing.Dir, Turing.Tape.move, Turing.Tape.write, Turing.Tape.head
```
def step (M : Machine Γ Λ) : Cfg Γ Λ → Option (Cfg Γ Λ)
| ⟨none, _⟩ => none
| ⟨some q, T⟩ => (M q T.1).map
    fun ⟨q', a⟩ ↦ ⟨q', match a with
    | Stmt.write a d => (T.write a).move d⟩

/-- The statement `Reaches M s₁ s₂` means that `s₂` is obtained
  starting from `s₁` after a finite number of steps from `s₂`. -/
```
Mentions: Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Turing.BusyBeaver.Machine.Reaches
def Turing.BusyBeaver.Machine.Reaches The statement Reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps from s₂ line 112 source
Source documentation
The statement Reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps from s₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg
Proof uses: Relation.ReflTransGen, Membership.mem, Option, Turing.BusyBeaver.Machine.step
1 instances, coercions and auxiliary constants left out.
```
def Reaches (M : Machine Γ Λ) : Cfg Γ Λ → Cfg Γ Λ → Prop := ReflTransGen fun a b ↦ b ∈ step M a
```
Mentions: Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Turing.BusyBeaver.Machine.step
def Turing.BusyBeaver.Machine.init The initial configuration line 115 source
Source documentation
The initial configuration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, List, Turing.BusyBeaver.Cfg
Proof uses: Turing.BusyBeaver.Cfg.mk, Option.some, Inhabited.default, Turing.Tape.mk₁
```
def init (l : List Γ) : Cfg Γ Λ := ⟨some default, Tape.mk₁ l⟩
```
Mentions: Turing.BusyBeaver.Cfg
def Turing.BusyBeaver.Machine.eval Evaluate a Turing machine on initial input to a final state, if it terminates line 119 source
Source documentation
Evaluate a Turing machine on initial input to a final state, if it terminates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, List, Part, Turing.ListBlank
Proof uses: Part.map, Turing.BusyBeaver.Cfg, Turing.Tape.right₀, Turing.BusyBeaver.Cfg.tape, StateTransition.eval, Turing.BusyBeaver.Machine.step, Turing.BusyBeaver.Machine.init
```
def eval (M : Machine Γ Λ) (l : List Γ) : Part (ListBlank Γ) :=
…
```
Mentions: Turing.BusyBeaver.Machine
def Turing.BusyBeaver.Machine.multiStep line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Nat, Option
Proof uses: Nat.iterate, Option.bind, Turing.BusyBeaver.Machine.step, Option.some
lemma Turing.BusyBeaver.Machine.multiStep_zero line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Eq, Option, Turing.BusyBeaver.Machine.multiStep, OfNat.ofNat, Nat, Option.some
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Turing.BusyBeaver.Machine.multiStep_one line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Eq, Option, Turing.BusyBeaver.Machine.multiStep, OfNat.ofNat, Nat, Turing.BusyBeaver.Machine.step
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Turing.BusyBeaver.Machine.multiStep_succ line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Nat, Eq, Option, Turing.BusyBeaver.Machine.multiStep, HAdd.hAdd, OfNat.ofNat, Option.bind, Turing.BusyBeaver.Machine.step
Proof uses: Eq.mpr, Nat.iterate, Option.some, id, congrArg, Turing.BusyBeaver.Machine.multiStep.eq_1, Function.comp, Nat.succ, Function.iterate_succ', Function.comp_apply, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Turing.BusyBeaver.Machine.multiStep_eq_none_mono line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Nat, Eq, Option, Turing.BusyBeaver.Machine.multiStep, Option.none, LE.le
Proof uses: Nat.le.rec, Nat.le, Eq.mpr, Nat.succ, Option.bind, Turing.BusyBeaver.Machine.step, id, congrArg, HAdd.hAdd, OfNat.ofNat, Turing.BusyBeaver.Machine.multiStep_succ, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Turing.BusyBeaver.Machine.IsHaltingInput M.IsHaltingInput l is the predicate that M is a halting configuration for M line 154 source
Source documentation
M.IsHaltingInput l is the predicate that M is a halting configuration for M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, List
Proof uses: Part.Dom, Turing.ListBlank, Turing.BusyBeaver.Machine.eval
```
def IsHaltingInput (l : List Γ) : Prop := (eval M l).Dom
```
Mentions: Turing.BusyBeaver.Machine.eval
def Turing.BusyBeaver.Machine.IsHaltingConfiguration M.HaltsAtConfiguration s is the predicate that M is a halting configuration for M line 161 source
Source documentation
M.HaltsAtConfiguration s is the predicate that M is a halting configuration for M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg
Proof uses: Eq, Bool, Option.isNone, Turing.BusyBeaver.Machine.step, Bool.true
```
def IsHaltingConfiguration (s : Cfg Γ Λ) : Prop := (step M s).isNone
```
Mentions: Turing.BusyBeaver.Cfg, Turing.BusyBeaver.Machine.step
class Turing.BusyBeaver.Machine.IsHalting The property that a Turing Machine M eventually halts when starting from an empty tape line 166 source
Source documentation
The property that a Turing Machine M eventually halts when starting from an empty tape

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine
```
class IsHalting : Prop where
…
```
def Turing.BusyBeaver.Machine.HaltsAfter The predicate that a machine starting at configuration s stops after at most n steps, i.e. reaches a configuration from which there are no defined transitions line 173 source
Source documentation
The predicate that a machine starting at configuration s stops after at most n steps, i.e. reaches a configuration from which there are no defined transitions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Nat
Proof uses: Eq, Option, Turing.BusyBeaver.Machine.multiStep, HAdd.hAdd, OfNat.ofNat, Option.none
3 instances, coercions and auxiliary constants left out.
```
def HaltsAfter (s : Cfg Γ Λ) (n : ℕ) : Prop :=
…
```
Mentions: Turing.BusyBeaver.Cfg
lemma Turing.BusyBeaver.Machine.haltsAfter_zero_iff line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Iff, Turing.BusyBeaver.Machine.HaltsAfter, OfNat.ofNat, Nat, Eq, Option, Turing.BusyBeaver.Machine.step, Option.none
Proof uses: Eq.mpr, Turing.BusyBeaver.Machine.multiStep, HAdd.hAdd, id, congrArg, Turing.BusyBeaver.Machine.HaltsAfter.eq_1, Nat.iterate, Option.bind, Option.some, Turing.BusyBeaver.Machine.multiStep.eq_1, Function.iterate_one, Option.bind_some, Iff.rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Turing.BusyBeaver.Machine.isHalting_iff_exists_haltsAt line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Iff, Turing.BusyBeaver.Machine.IsHalting, Exists, Nat, Turing.BusyBeaver.Machine.HaltsAfter, Turing.BusyBeaver.Machine.init, List.nil
Proof uses: Iff.intro, Iff.mpr, Eq, Option, Turing.BusyBeaver.Cfg, Nat.iterate, Option.bind, Turing.BusyBeaver.Machine.step, HAdd.hAdd, OfNat.ofNat, Option.some, Option.none, Part.Dom, StateTransition.eval, StateTransition.eval_dom_iff, Turing.BusyBeaver.Machine.IsHalting.halts, Turing.BusyBeaver.Machine.IsHalting.mk, Iff.mp
3 instances, coercions and auxiliary constants left out.
lemma Turing.BusyBeaver.Machine.exists_of_not_haltsAfter line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Turing.BusyBeaver.Cfg, Nat, Not, Turing.BusyBeaver.Machine.HaltsAfter, Exists, Turing.Tape, Eq, Option, Turing.BusyBeaver.Machine.multiStep, Option.some, Turing.BusyBeaver.Cfg.mk
Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, Ne, id, implies_congr, binderNameHint, Eq.trans, forall_congr, Eq.refl, HAdd.hAdd, OfNat.ofNat, Option.none, congrArg, Turing.BusyBeaver.Machine.HaltsAfter.eq_1, Option.bind, Turing.BusyBeaver.Machine.step, Turing.BusyBeaver.Machine.multiStep_succ, Or, Option.eq_none_or_eq_some, of_eq_true and 14 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Turing.BusyBeaver.Machine.not_isHalting_iff_forall_isSome_multiStep line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Iff, Not, Turing.BusyBeaver.Machine.IsHalting, Nat, Eq, Bool, Option.isSome, Turing.BusyBeaver.Cfg, Turing.BusyBeaver.Machine.multiStep, Turing.BusyBeaver.Machine.init, List.nil, HAdd.hAdd, OfNat.ofNat, Bool.true
Proof uses: Eq.mpr, Exists, Turing.BusyBeaver.Machine.HaltsAfter, id, congrFun', congrArg, Option, Option.none, Ne, forall_congr, Iff.rfl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Turing.BusyBeaver.Machine.not_isHalting_of_forall_isSome line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Exists, Turing.BusyBeaver.Stmt, Eq, Option, Prod, Option.some, Prod.mk, Not, Turing.BusyBeaver.Machine.IsHalting
Proof uses: Eq.mpr, Nat, Bool, Option.isSome, Turing.BusyBeaver.Cfg, Turing.BusyBeaver.Machine.multiStep, Turing.BusyBeaver.Machine.init, List.nil, HAdd.hAdd, OfNat.ofNat, Bool.true, id, congrArg, propext, Turing.BusyBeaver.Machine.not_isHalting_iff_forall_isSome_multiStep, Nat.recAux, Inhabited.default, Turing.Tape.head, Turing.Tape.mk₁, of_eq_true and 21 more
6 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Turing.BusyBeaver.Machine.haltingNumber line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, ENat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Nat, Turing.BusyBeaver.Machine.HaltsAfter, Turing.BusyBeaver.Machine.init, List.nil, Eq
9 instances, coercions and auxiliary constants left out.
theorem Turing.BusyBeaver.Machine.haltingNumber_def line 220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Inhabited, Turing.BusyBeaver.Machine, Nat, Exists, Turing.BusyBeaver.Cfg, Eq, Option, Turing.BusyBeaver.Machine.multiStep, Turing.BusyBeaver.Machine.init, List.nil, Option.some, HAdd.hAdd, OfNat.ofNat, Option.none, ENat, Turing.BusyBeaver.Machine.haltingNumber
Proof uses: IsGLB.sInf_eq, Set.ofPred, Turing.BusyBeaver.Machine.HaltsAfter, IsLeast.isGLB, And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Eq.mpr, id, congrArg, Turing.BusyBeaver.Machine.HaltsAfter.eq_1, rfl, LE.le, ENat.recTopCoe, Top.top, le_top, Eq.symm, Decidable.byContradiction and 16 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.