OpenFrontiers
Join
← Back to the index
OP-9978Status unassessedLogic and foundations

Busy Beaver

Busy Beaver

MSC 03 · Mathematical logic and foundations

Inferred from the community field; finer classification has not been reviewed.

Specialist source · status unassessedAs of 2026-09-10Source & evidence ↓
Read original source ↗ 0Submit progressLean 4 ↓Discussion (0)

Problem statement

BB_6

Determine the value of the Busy Beaver function at n = 6.

Lean 4

No Lean submitted

Formal statement

Lean 4
/-
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 FormalConjecturesUtil

/-!
# Busy 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:*

- [The Busy Beaver Challenge](https://wiki.bbchallenge.org/wiki/Main_Page)
-/

universe u v

open Turing BusyBeaver

namespace BusyBeaver

structure 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.IsHalting

instance {n : ℕ} {M : Candidate n} : Fintype M.Γ := M.Γ_fintype
instance {n : ℕ} {M : Candidate n} : Fintype M.Λ := M.Λ_fintype
instance {n : ℕ} {M : Candidate n} : Inhabited M.Γ := M.Γ_inhabited
instance {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} := by
  sorry

/-- The value of the Busy Beaver function for 1 state is 1. -/
@[category test, AMS 3]
theorem BB_1 : BB 1 = 1 := by
  sorry

/-- The value of the Busy Beaver function for 2 states is 6. -/
@[category textbook, AMS 3]
theorem BB_2 : BB 2 = 6 := by
  sorry

/-- The value of the Busy Beaver function for 3 states is 21. -/
@[category textbook, AMS 3]
theorem BB_3 : BB 3 = 21 := by
  sorry

/-- The value of the Busy Beaver function for 4 states is 107. -/
@[category textbook, AMS 3]
theorem BB_4 : BB 4 = 107 := by
  sorry

/-- The value of the Busy Beaver function for 5 states is 47176870. -/
@[category research solved, AMS 3]
theorem BB_5 : BB 5 = 47176870 := by
  sorry

/--
Determine the value of the Busy Beaver function at n = 6.
-/
@[category research open, AMS 3]
theorem BB_6 : BB 6 = answer(sorry) := by
  sorry

end BusyBeaver

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.

Proofs & verification

No Lean has been submitted for this problem yet. A Lean file can be attached to a submission for review, though with no target here it cannot be machine-checked.

Share a formalization →Verification guide ↗

Background

Source snapshot inspected on 10 September 2026. Subsequent research status and the accuracy of source formalizations have not been independently certified.

Fixed commit b82b08faa9006484021c12005ab41287fb2ffb69. This file contains 1 source-labeled research-open declarations. Other declarations in the attached file can be definitions, solved results or tests. The file is preserved as source material; it has not been compiled or proved by this import.

Copyright The Formal Conjectures Authors. Code: Apache-2.0; other original material: CC BY 4.0. Third-party sources retain their own licenses. Original source files and notices preserved.

References
  1. [1]Formal Conjectures — Busy Beaver link
  2. [2]Original reference cited in the formalization link

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Sign in to run an attempt. New accounts start with enough credits for ten.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.

Sign in to add a note.