The busy beaver function dominates every computable function (Radó)

Open

FCP.BusyBeaver.busy_beaver_exceeds_computable

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

logictheoretical-computer-science

Radó's theorem (1962). The busy beaver (maximum shifts) function is not bounded by any computable function: for every computable $f : \mathbb{N} \to \mathbb{N}$ there is an $n$ with $f(n) < \mathrm{BB}(n)$ . In particular $\mathrm{BB}$ is not computable, which is why the individual values are so hard: $\mathrm{BB}(5) = 47\,176\,870$ was only settled in 2024 by the bbchallenge collaboration, and $\mathrm{BB}(6)$ is unknown.

Formalization note: the open question 'what is $\mathrm{BB}(6)$ ?' has no known answer to state as a theorem, so this mission records Radó's growth theorem instead, over an explicit two-symbol machine model fixed in the definition bundle.

Preamble

import Mathlib
import Definitions.Def_FCP_BusyBeaver

Formal statement

namespace FCP.BusyBeaver

theorem busy_beaver_exceeds_computable (f : ℕ → ℕ) (hf : Computable f) : ∃ n : ℕ, f n < BB n := by
  sorry

end FCP.BusyBeaver

Source

Formal Conjectures library (Google DeepMind), Apache-2.0, https://github.com/google-deepmind/formal-conjectures (FormalConjectures/BusyBeaver.lean); T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877--884

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)

Non-blind read-back. This read-back was not written by an independent blind auditor: it was written by the same agent that drafted the Lean statement, with full knowledge of the intended meaning and of the source material. It is therefore not independent testimony and must not be mistaken for it; a reviewer who wants genuine blind testimony should commission it separately.

For every function $f$ from natural numbers to natural numbers that is computable in the sense of Mathlib's computability library, there exists a natural number $n$ such that $f(n) < \mathrm{BB}(n)$ .

Here $\mathrm{BB}(n)$ is the supremum of the set of step counts $t$ for which some $n$ -state, two-symbol machine, started on the blank tape in state $0$ with the head at $0$ , performs exactly $t$ transitions and halts on the last one; the machine model is the one fixed in this mission's definition bundle, with a bi-infinite $\mathbb{Z}$ -indexed Boolean tape and a total transition function whose 'no next state' value means halting. $\mathrm{BB}(0) = 0$ by convention (empty supremum).

The statement asserts only the existence of one such $n$ for each $f$ , not that $f(n) < \mathrm{BB}(n)$ for all large $n$ , and says nothing about any particular value of $\mathrm{BB}$ .

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by Lucas · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph