/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilBusy Beaver
The Busy Beaver problem asks for the maximum number of steps that an n-state, 2-symbol Turing machine can take before halting, when started on an empty tape.
References:
universe u vopen Turing BusyBeavernamespace BusyBeaverstructure Candidate (n : ℕ) where
Γ : Type
Λ : Type
Γ_fintype : Fintype Γ
Γ_card : Fintype.card Γ = 2
Γ_inhabited : Inhabited Γ
Λ_fintype : Fintype Λ
Λ_card : Fintype.card Λ = n
Λ_inhabited : Inhabited Λ
M : Machine Γ Λ
M_isHalting : M.IsHaltinginstance {n : ℕ} {M : Candidate n} : Fintype M.Γ := M.Γ_fintypeinstance {n : ℕ} {M : Candidate n} : Fintype M.Λ := M.Λ_fintypeinstance {n : ℕ} {M : Candidate n} : Inhabited M.Γ := M.Γ_inhabitedinstance {n : ℕ} {M : Candidate n} : Inhabited M.Λ := M.Λ_inhabited
BB(n) is the n-th Busy Beaver number.
This is the maximum shifts function, not the "number of ones function"
noncomputable def BB (n : ℕ) : ℕ :=
sSup { N | ∃ C : Candidate n, C.M.haltingNumber = N}
To compute BB n, we need only consider machines with states and symbols indexed in Fin.
@[category API, AMS 3]
theorem sanity_check (n : ℕ) [NeZero n] :
BB n = sSup {N | ∃ (M : Machine (Fin 2) (Fin n)) (_ : M.IsHalting),
M.haltingNumber = N} := n:ℕinst✝:NeZero n⊢ ↑(BB n) = sSup {N | ∃ M, ∃ (_ : M.IsHalting), M.haltingNumber = N}
All goals completed! 🐙The value of the Busy Beaver function for 1 state is 1.
@[category test, AMS 3]
theorem BB_1 : BB 1 = 1 := ⊢ BB 1 = 1
All goals completed! 🐙The value of the Busy Beaver function for 2 states is 6.
@[category textbook, AMS 3]
theorem BB_2 : BB 2 = 6 := ⊢ BB 2 = 6
All goals completed! 🐙The value of the Busy Beaver function for 3 states is 21.
@[category textbook, AMS 3]
theorem BB_3 : BB 3 = 21 := ⊢ BB 3 = 21
All goals completed! 🐙The value of the Busy Beaver function for 4 states is 107.
@[category textbook, AMS 3]
theorem BB_4 : BB 4 = 107 := ⊢ BB 4 = 107
All goals completed! 🐙The value of the Busy Beaver function for 5 states is 47176870.
@[category research solved, AMS 3]
theorem BB_5 : BB 5 = 47176870 := ⊢ BB 5 = 47176870
All goals completed! 🐙Determine the value of the Busy Beaver function at n = 6.
@[category research open, AMS 3]
theorem BB_6 : BB 6 = answer(sorry) := ⊢ BB 6 = sorry
All goals completed! 🐙end BusyBeaver