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).
• 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---4LB1RA4RA_2LB2LA3RA4LB0RB (bbch).
• 1RB---4LB0LA4RA_2LB2LA3RA4LB0RB (bbch).
• 1RB---0RB0LA2RA_2LB2LA3RA4LB0LB (bbch). Shift overflow counter, potential Cryptid
• 1RB3LA1LA1RA3RA_2LB2RA---4RB1LB (bbch). Potential Cryptid
• 1RB3LA1LA1RA1RA_2LB2RA---4RB1LB (bbch). Potential Cryptid
• 1RB3LA1LA4LA2RA_2LB2RA---0RA0RB (bbch).
• 1RB4RA1LA4RB2LA_2LB3LA1RB2RA--- (bbch).
• 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA (bbch).
• 1RB4LA1RA1RB1LA_2LB3LA---4RA2RB (bbch). Basic long. analysis by @dyuan
• 1RB---4RB2RB4LA_2LB3LA3LB0RA0RB (bbch). Bouncer + chaotic counter
• 1RB2RB3LA4LA1LA_2LB3RA---4RA1RB (bbch).
• 1RB3RB3LA4LA2RB_2LB3RA---1RA1LA (bbch).
• 1RB2LA4LA1RA1LA_2LB3RB4RB---2RA (bbch).
• 1RB4RB4RA1LA3LA_1LB2LA3RB2RB--- (bbch).
• 1RB3RA3RB4LA1LA_1LB2LA1LA---1RB (bbch). Potentially halt
• 1RB2RA4LA1RB4RB_1LB2LA3RA---0LB (bbch).
• 1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- (bbch).
• 1RB3LA1LA2RB2LB_1LB2RA4RA0RB--- (bbch).
• 1RB2LA0RB0LB3LB_2LA4RB3RA0RA--- (bbch).
• 1RB2RA3LB---2LB_2LA0LA4RB0RB1LA (bbch). 30% chance of beating current champion
• 1RB2RA3LB4LA---_2LA0RB1LA2RB0RA (bbch). Analysis by @dyuan01 and @Legion
• 1RB2RA3LA---2LB_2LA4RA4RB0RB0LA (bbch). Spaghetti analysis by @nerdyjoe
• 1RB2RA3LA4LA2RB_2LA---3LB1RA3RA (bbch). Bouncer + chaotic counter
• 1RB2RA3LA4LA2RB_2LA3RB---0RA1LA (bbch). Longitudinal analysis suggests chaotic
• 1RB3LA1RA4LA2RA_2LA---1LA0RA3RB (bbch). Longitudinal analysis suggests chaotic. More analysis by mxdys
• 1RB3LA3LB0RB0LA_2LA4RB1LB1RA--- (bbch).
• 1RB3LA1LA2RB2RA_2LA4RA3LB1RA--- (bbch).
• 1RB3LA3LA0RB2LB_2LA4LA4RA2RA--- (bbch). Analysis by @mxdys
• 1RB2LB3LA0RA1LB_2LA4RA3RB3LA--- (bbch). Analysis by @nerdyjoe
• 1RB2RB---0LB3LA_2LA2LB3RB4RB1LB (bbch). Longitudinal analysis suggests chaotic
• 1RB2RB4LA2RA1LA_2LA4RA3LA---3RA (bbch). Longitudinal analysis suggests chaotic
• 1RB3LB---4LA1RB_2LA4LA4LB3RB1RA (bbch). Potential cryptid - Analysis by @mxdys
• 1RB3LB0RB---2LB_2LA3RA4RB2RB0LA (bbch). Analysis by @mxdys
• 1RB3LB4LA0LB---_2LA0LA1RB0RA3RA (bbch).
• 1RB3RB---4RA2RA_2LA2RA3LB4LB1LB (bbch).
• 1RB3RB1LB2RA---_2LA2RB1LA4LB0RA (bbch).
• 1RB2LA0RB1LA3LB_1LA3LB1RA4RA--- (bbch).
• 1RB2LA0RB4LB1RA_1LA3RA1RA---0LA (bbch).
• 1RB2LA0RB---4LA_1LA3LA1RA4RA1LB (bbch).
• 1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch).
• 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?
• 1RB2RA3LA4LA2RB_2LA3RA---0RA1LA (bbch). Longitudinal analysis suggest chaotic
• 1RB---3LB4RB0LA_2LB3LA3RB4RA0RA (bbch).

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 ~9e1167 steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2LB (bbch). Simulated for ~1.3e1094 steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1RB (bbch). Simulated for ~9.8e1226 steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1LB (bbch). Simulated for ~3.0e1140 steps by @hipparcos, hasn't halted yet
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0RB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0LB (bbch). Simulated for ~2.6e889 steps by @hipparcos, hasn't halted yet
• 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
• 1RB0RB3LA4LA2RA_2LB3RA---3RA4RB (bbch). BMO problem 3
• 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA (bbch). Nonhalting argument 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
• 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

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