structure BusyBeaver.Candidate (n : ℕ) : Type 1

• Γ : Type
• Λ : Type
• Γ_fintype : Fintype self.Γ
• Γ_card : Fintype.card self.Γ = n
• Γ_inhabited : Inhabited self.Γ
• Λ_fintype : Fintype self.Λ
• Λ_card : Fintype.card self.Λ = 2
• Λ_inhabited : Inhabited self.Λ
• M : Turing.BusyBeaver.Machine self.Γ self.Λ
• M_isHalting : self.M.IsHalting

instance BusyBeaver.instFintypeΓ {n : ℕ} {M : Candidate n} : Fintype M.Γ

Equations

• BusyBeaver.instFintypeΓ = M.Γ_fintype

instance BusyBeaver.instFintypeΛ {n : ℕ} {M : Candidate n} : Fintype M.Λ

Equations

• BusyBeaver.instFintypeΛ = M.Λ_fintype

instance BusyBeaver.instInhabitedΓ {n : ℕ} {M : Candidate n} : Inhabited M.Γ

Equations

• BusyBeaver.instInhabitedΓ = M.Γ_inhabited

instance BusyBeaver.instInhabitedΛ {n : ℕ} {M : Candidate n} : Inhabited M.Λ

Equations

• BusyBeaver.instInhabitedΛ = M.Λ_inhabited

noncomputable def BusyBeaver.BB (n : ℕ) : ℕ

BB(n) is the n-th Busy Beaver number. This is the maximum shifts function, not the "number of ones function"

Equations

• BusyBeaver.BB n = sSup {N : ℕ | ∃ (C : BusyBeaver.Candidate n), C.M.haltingNumber = ↑N}

theorem sanity_check (n : ℕ) [NeZero n] : ↑(BusyBeaver.BB n) = sSup {N : PartENat | ∃ (M : Turing.BusyBeaver.Machine (Fin n) (Fin 2)) (_ : M.IsHalting), M.haltingNumber = N}

To compute BB n, we need only consider machines with states and symbols indexed in Fin.

theorem BB_1 : BusyBeaver.BB 1 = 1

theorem BB_2 : BusyBeaver.BB 2 = 6

theorem BB_3 : BusyBeaver.BB 3 = 21

theorem BB_4 : BusyBeaver.BB 4 = 107

theorem BB_5 : BusyBeaver.BB 5 = 47176870