BB(6): what is known about the sixth Busy Beaver (2026)
BB(5) = 47,176,870 is proved; BB(6) is out of reach — its champion runs for more than 10↑↑10↑↑10↑↑8 steps and some undecided machines encode Collatz-like problems. The current status, the open machines, and where contributions help.
Updated 2026-10-03 · CC BY 4.0
The Busy Beaver function asks a simple question: among all Turing machines with n states (and two symbols) that eventually halt when started on a blank tape, which runs the longest? That maximum number of steps is S(n), usually written BB(n); the maximum number of 1s left on the tape is Σ(n). Both grow faster than any computable function, so each new value is a small miracle of computer-assisted proof. This guide summarises where BB(6) stands as of October 2026.
The values we know
| n | BB(n) = S(n) | Σ(n) | Proved |
|---|---|---|---|
| 1 | 1 | 1 | trivial |
| 2 | 6 | 4 | Radó (1962) |
| 3 | 21 | 6 | Lin and Radó (1965) |
| 4 | 107 | 13 | Brady (1983) |
| 5 | 47,176,870 | 4,098 | bbchallenge collaboration (2024) |
| 6 | > 10↑↑10↑↑10↑↑8 | > 10↑↑10↑↑10↑↑8 | open |
The BB(5) proof, announced in 2024, is a formal proof in the Coq proof assistant (now called Rocq): it classifies every relevant 5-state machine as halting or non-halting using deciders — programs that recognise a kind of non-halting behaviour — whose correctness is itself proved in Coq. The champion machine had been found by Heiner Marxen and Jürgen Buntrock in 1989; the hard part was proving that nothing beats it. A paper describing the proof, Determination of the fifth Busy Beaver value, appeared in September 2025.
How big is BB(6)?
Lower bounds for six states come from explicit machines that halt after an enormous number of steps. The bbchallenge wiki records the history:
| Year | Lower bound | Found by |
|---|---|---|
| 1964 | S(6) ≥ 436, Σ(6) ≥ 35 | M. W. Green |
| 1990 | S(6) ≥ 13,122,572,797, Σ(6) ≥ 136,612 | Marxen and Buntrock |
| 2010 | Σ(6) > 3.5 × 10^18267 | Pavel Kropitz |
| 2022 | S(6) > 10↑↑15 | Shawn Ligocki and Pavel Kropitz |
| 2025 | S(6) > Σ(6) > 10↑↑10↑↑10↑↑8 | mxdys |
Here ↑↑ is tetration: 10↑↑3 = 10^10^10, a tower of three 10s. The 2025 champion's step count is a tower of tetrations — far beyond anything that can be simulated step by step. These machines are analysed by finding the rules their configurations follow and proving that the machine halts after a computable, if absurd, number of rule applications.
Why BB(6) may never be determined
To prove BB(6) you must decide, for every 6-state machine, whether it halts. In June 2024 a machine nicknamed Antihydra (1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA) was found whose behaviour reduces to iterating a Collatz-like map, roughly n ↦ ⌊3n/2⌋ + 2, together with a parity condition that decides whether it ever halts. The trajectory looks like a random walk with a drift away from halting, so it almost certainly runs forever — but proving that is a problem of the same kind as the Collatz conjecture, for which no method is known. It has been simulated to 2^38 rule steps.
Antihydra is one of about ten known cryptids: machines whose halting is equivalent to an open problem in number theory. Unless someone makes progress on Collatz-type questions, BB(6) cannot be pinned down.
What is still undecided
Most 6-state machines are decided by the same kinds of deciders that solved BB(5). As of late September 2026, the bbchallenge wiki lists about 815 holdouts (counted up to equivalence; an informal count gives 998), most of them simulated to 10^13 steps without halting. Each holdout needs either a new decider that recognises its behaviour or an individual proof.
Where contributions help
The Busy Beaver holdouts problem on Cairn Commons collects work on the 6-state frontier. Useful, checkable contributions include:
- A new decider with code and a certificate format, that resolves additional holdouts.
- A non-halting proof for a named machine, in standard notation such as the one above, linked to its bbchallenge page.
- Analysis of a cryptid: reducing it to a cleaner number-theoretic statement, or proving partial results about the induced map.
- Formal proofs. The Lean formalisation problem asks for a Lean 4 proof of BB(5) checked by the kernel alone. A community port already claims BB(5) in Lean using
native_decide, which trusts compiled code; removing that dependency, and formalising BB(2,4) = 3,932,964 (proved in Coq), are open.
Results that bear on the bbchallenge effort should also be reported there; the collaboration's Discord and wiki are where the holdout list is maintained.
Sources
- The bbchallenge Collaboration, Determination of the fifth Busy Beaver value, arXiv 2509.12337 (2025).
- BB(6) and Antihydra, bbchallenge wiki (accessed October 2026).
- bbchallenge.org.