BB(2,5)

The 2-state, 5-symbol Busy Beaver problem, BB(2,5), is unsolved. With the discovery of the Cryptid machine Hydra in April 2024, we now know that we must solve a Collatz-like problem in order to solve BB(2,5) and thus BB(2,5) is Hard.

The current BB(2,5) champion 1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ (bbch) was discovered by Daniel Yuan in June 2024, proving the lower bounds:

$$S(2,5)>\mathrm{\Sigma }(2,5)>10^{10^{10^{3314360}}}>10\uparrow \uparrow 4$$

Cryptids

Known Cryptids:

• 1RB3RB---3LA1RA_2LA3RA4LB0LB0LA (bbch), known as Hydra
• 1RB3RB---3LA1RA_2LA3RA4LB0LB1LB (bbch), known as the Bonus Cryptid

Potential Cryptids:

• 1RB---0RB0LA2RA_2LB2LA3RA4LB0LB (bbch). Shift overflow counter
• 1RB3LA1LA1RA3RA_2LB2RA---4RB1LB (bbch).
• 1RB3LA1LA1RA1RA_2LB2RA---4RB1LB (bbch).
• 1RB3LB---4LA1RB_2LA4LA4LB3RB1RA (bbch). Analysis by @mxdys

Top Halters

Some of the longest running halting BB(2,5) TMs are:

Standard format	(approximate) runtime
1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ (bbch)	$10\uparrow \uparrow 4.8142742$
1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA (bbch)	$>10^{38033}$

Certified progress

In April 2024, Shawn Ligocki publicly released a list of 23,411 undecided BB(2,5) machines. Justin Blanchard then made substantial progress over the course of the next month, reducing the list to 499 holdouts by late May 2024. In June 2024, @mxdys cut down the list to 273 using halting and inductive deciders, and again to 217 using CTL. In February 2025, @mxdys ran a decider pipeline in Rocq that resulted in only 173 holdouts. Since then, additional machines have been proven in Rocq using both deciders and individual proofs.

On 29 Mar 2025, @mxdys published a list of 83 holdouts that withstood state-of-the-art Rocq deciders.

Over the course of 5 months, @mxdys added 8 machines to Rocq¹²³⁴⁵, lowering the certified holdout count to 75. There are 11 informal arguments, lowering the informal holdout count to 64.

Holdouts

This section is based on the list of 83 holdouts published by @mxdys, and includes further progress as of 25 October 2025.

Cryptids

• 1RB3RB---3LA1RA_2LA3RA4LB0LB0LA (bbch). Hydra
• 1RB3RB---3LA1RA_2LA3RA4LB0LB1LB (bbch). Bonus Cryptid

Unsolved

• 1RB---4LB0LA4RA_2LB2LA3RA4LB0RB (bbch).
• 1RB3LA1LA4LA2RA_2LB2RA---0RA0RB (bbch).
• 1RB4RA1LA4RB2LA_2LB3LA1RB2RA--- (bbch).
• 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA (bbch).
• 1RB2RB3LA4LA1LA_2LB3RA---4RA1RB (bbch).
• 1RB3RB3LA4LA2RB_2LB3RA---1RA1LA (bbch).
• 1RB2LA4LA1RA1LA_2LB3RB4RB---2RA (bbch).
• 1RB4RB4RA1LA3LA_1LB2LA3RB2RB--- (bbch).
• 1RB2RA4LA1RB4RB_1LB2LA3RA---0LB (bbch).
• 1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- (bbch).
• 1RB3LA3LB0RB0LA_2LA4RB1LB1RA--- (bbch).
• 1RB3LA1LA2RB2RA_2LA4RA3LB1RA--- (bbch).
• 1RB3RB---4RA2RA_2LA2RA3LB4LB1LB (bbch).
• 1RB2LA0RB1LA3LB_1LA3LB1RA4RA--- (bbch).
• 1RB2LA0RB4LB1RA_1LA3RA1RA---0LA (bbch).
• 1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch).
• 1RB---3LB4RB0LA_2LB3LA3RB4RA0RA (bbch).
• 1RB3LB---4LA1RB_2LA4LA4LB3RB1RA (bbch). Potential Cryptid - Analysis by @mxdys
• 1RB3LA1LA1RA3RA_2LB2RA---4RB1LB (bbch). Potential Cryptid
• 1RB3LA1LA1RA1RA_2LB2RA---4RB1LB (bbch). Potential Cryptid
• 1RB---0RB0LA2RA_2LB2LA3RA4LB0LB (bbch). Potential Cryptid - Shift overflow counter
• 1RB2RA3LB---2LB_2LA0LA4RB0RB1LA (bbch). 30% chance of beating current champion
• 1RB3LA1LA2RB2LB_1LB2RA4RA0RB--- (bbch). Block analysis by @dyuan by "impurity score"
• 1RB---4LB1RA4RA_2LB2LA3RA4LB0RB (bbch). Analysis by Andrew Ducharme and @mxdys
• 1RB---4RB2RB4LA_2LB3LA3LB0RA0RB (bbch). Bouncer + chaotic counter
• 1RB2LA0RB0LB3LB_2LA4RB3RA0RA--- (bbch). Analysis by Peacemaker II
• 1RB2RA3LB4LA---_2LA0RB1LA2RB0RA (bbch). Analysis by @dyuan01 and @Legion
• 1RB2RA3LA---2LB_2LA4RA4RB0RB0LA (bbch). Spaghetti, analysis by @nerdyjoe
• 1RB2RA3LA4LA2RB_2LA---3LB1RA3RA (bbch). Bouncer + chaotic counter
• 1RB3LA3LA0RB2LB_2LA4LA4RA2RA--- (bbch). Analysis by @mxdys
• 1RB2LB3LA0RA1LB_2LA4RA3RB3LA--- (bbch). Analysis by @nerdyjoe
• 1RB3LB0RB---2LB_2LA3RA4RB2RB0LA (bbch). Analysis by @mxdys
• 1RB3LB4LA0LB---_2LA0LA1RB0RA3RA (bbch). Analysis by Peacemaker II
• 1RB3RB1LB2RA---_2LA2RB1LA4LB0RA (bbch). Analysis by Legion and @dyuan
• 1RB2LA0RB---4LA_1LA3LA1RA4RA1LB (bbch). Analysis by @racheline
• 1RB4LA1RA1RB1LA_2LB3LA---4RA2RB (bbch). Basic long. analysis by @dyuan
• 1RB3RA3RB4LA1LA_1LB2LA1LA---1RB (bbch). Long. analysis by @dyuan suggests chaotic, potentially halt
• 1RB3LA1RA4LA2RA_2LA---1LA0RA3RB (bbch). Chaotic via long. analysis. More analysis by mxdys
• 1RB2RB4LA2RA1LA_2LA4RA3LA---3RA (bbch). Chaotic via long. analysis. Probviously nonhalting
• 1RB2RA3LA4LA2RB_2LA3RA---0RA1LA (bbch). Chaotic via long. analysis
• 1RB2RA3LA4LA2RB_2LA3RB---0RA1LA (bbch). Chaotic via long. analysis
• 1RB2RB---0LB3LA_2LA2LB3RB4RB1LB (bbch). Chaotic via long. analysis
• 1RB2LA4RA1LA3LA_0LA2RB3RB2LB--- (bbch). 1D CA-like. Analysis by @dyuan and @mxdys
• 1RB2LA4RA1LA3LA_0LA3RB3LB2RB--- (bbch). 1D CA-like
• 1RB2LA1LA4RA2LA_0LA3RB3LB2RB--- (bbch). 1D CA-like
• 1RB2LA3LA4RA1LA_0LA3LB3RB1RB--- (bbch). 1D CA-like
• 1RB2LA3LB4LB---_0LA4LB3RA4LA0RB (bbch). Fractal?

The 15 grandchildren of 1RB2LA0RB1LB_1LA3RA1RA--- (bbch)

• 1RB2LA0RB1LB0LB_1LA3RA1RA4RA--- (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4RB0LB (bbch).

which includes the family 1RB2LA0RB1LB---_1LA3RA1RA4LB---. See this thread for more details.

• 1RB2LA0RB1LB---_1LA3RA1RA4LB2RB (bbch). Simulated for $9*10^{1167}$ steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2LB (bbch). Simulated for $1.3*10^{1094}$ steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1RB (bbch). Simulated for $9.8*10^{1226}$ steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1LB (bbch). Simulated for $3*10^{1140}$ steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0LB (bbch). Simulated for $2.6*10^{889}$ steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0RB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB3RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2LA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1LA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0LA (bbch).

Solved with moderate rigor

• 1RB1RB3LA4LA2RA_2LB3RA---3RA4RB (bbch). BMO problem 3 by @dyuan
• 1RB0RB3LA4LA2RA_2LB3RA---3RA4RB (bbch). BMO problem 3 by @dyuan
• 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (bbch). Longitudinal analysis by @Legion implies halting
• 1RB3LA4LA1LA2RA_2LA4RB---0RA0LA (bbch). Longitudinal analysis by @Legion implies halting
• 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch). Longitudinal analysis by @Legion implies halting
• 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB (bbch). Nonhalting argument by @racheline
• 1RB2LA0LB1LA2RA_0LA3RA1RA4LB--- (bbch). Nonhalting argument by Peacemaker II
• 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA (bbch). Nonhalting argument by @dyuan
• 1RB3RA2LB1LB1RB_2LA2RA4LA1LA--- (bbch). Dekaheptoid, - Unverified nonhalting proof by @dyuan
• 1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch). Dekaheptoid, - Unverified nonhalting proof by @dyuan
• 1RB0RA3LA4LA2RA_2LB3LA---4RA3RB (bbch). BMO problem 3 variant - Nonhalting argument by @dyuan

Formally proven

• 1RB2RA3LA4LA2RB_2LA0RA---0RA1LA (bbch). Rocq-decided by @mxdys. Longitudinal analysis by Legion implies nonhalting
• 1RB2RA3LA4RB---_2LA3RB3RA1LB3LB (bbch). Rocq-decided by @mxdys. Halting argument by @dyuan
• 1RB3LA4RB0RB2LA_1LB2LA3LA1RA--- (bbch). Rocq-decided by @mxdys. Current champion
• 1RB3RA4LB2RA2RB_2LA---3LA0LB1LA (bbch). Rocq-decided by @mxdys.
• 1RB3RB---0RA2RB_2LA4RA3LB1LB1LA (bbch). Rocq-decided by @mxdys.
• 1RB0LB2LA4LB3LA_2LA---3RA4RB2RB (bbch). Rocq-decided by @mxdys
• 1RB2LA1RA---1LA_1LA4RB3LB0RB2RB (bbch). Rocq-decided by @mxdys
• 1RB2LA3LA4RA0LA_1LA3RB1RB1LB--- (bbch). Rocq-decided by @mxdys