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)>\Sigma (2,5)>10^{10^{10^{3\,314\,360}}}>10\uparrow \uparrow 4$$

If it turns out to be the actual champion, it would the only known champion machine that exhibits Counter behavior.

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)

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 Coq that resulted in only 173 holdouts. Since then, additional machines have been proven in Coq using both deciders and individual proofs.

On 29 Mar 2025, @mxdys published a list of 83 holdouts that withstood state-of-the-art Coq deciders. Some of these machines were already decided before.

Holdouts

This section is based on @mxdys's March 2025 holdouts list of 83 TMs.

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). BMO 3 variant?
• 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
• 1RB3LA3LB0RB0LA_2LA4RB1LB1RA--- (bbch).
• 1RB3LA1LA2RB2RA_2LA4RA3LB1RA--- (bbch).
• 1RB3LA3LA0RB2LB_2LA4LA4RA2RA--- (bbch).
• 1RB3RA2LB1LB1RB_2LA2RA4LA1LA—-- (bbch). Skelet 17-like
• 1RB3RA4LB2RA2RB_2LA---3LA0LB1LA (bbch).
• 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). Longitudinal analysis suggests chaotic
• 1RB3LB0RB---2LB_2LA3RA4RB2RB0LA (bbch).
• 1RB3LB4LA0LB---_2LA0LA1RB0RA3RA (bbch).
• 1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch). Skelet 17-like
• 1RB3RB---4RA2RA_2LA2RA3LB4LB1LB (bbch).
• 1RB3RB---0RA2RB_2LA4RA3LB1LB1LA (bbch).
• 1RB3RB1LB2RA---_2LA2RB1LA4LB0RA (bbch).
• 1RB2LA0RB1LA3LB_1LA3LB1RA4RA--- (bbch).
• 1RB2LA0RB4LB1RA_1LA3RA1RA---0LA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4RB0LB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2RB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2LB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1RB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1LB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0RB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0LB (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB3RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB2LA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB1LA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0RA (bbch).
• 1RB2LA0RB1LB---_1LA3RA1RA4LB0LA (bbch).
• 1RB2LA0RB1LB0LB_1LA3RA1RA4RA--- (bbch).
• 1RB2LA0RB---4LA_1LA3LA1RA4RA1LB (bbch).
• 1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch).
• 1RB2LA4RA1LA3LA_0LA2RB3RB2LB--- (bbch). 1D CA-like
• 1RB2LA4RA1LA3LA_0LA3RB3LB2RB--- (bbch). 1D CA-like
• 1RB2LA1LA4RA2LA_0LA3RB3LB2RB--- (bbch). 1D CA-like
• 1RB2LA3LA4RA1LA_0LA3LB3RB1RB--- (bbch). 1D CA-like
• 1RB2LA0LB1LA2RA_0LA3RA1RA4LB—-- (bbch). Potential bouncer
• 1RB2LA3LB4LB---_0LA4LB3RA4LA0RB (bbch). Fractal?

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

Formally proven

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