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
• 1RB2RA3LB---2LB_2LA0LA4RB0RB1LA (bbch). Probviously halting. 1/8 chance of beating champ.

Top Halters

The 20 longest running known halting BB(2,5) TMs are:

Standard format	(approximate) runtime	Discoverer
1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ (bbch)	$10\uparrow \uparrow 4.8142742$	Daniel Yuan
1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA (bbch)	$>10^{38033}$	Pavel Kropitz
1RB2LA1RA2LB2LA_0LA2RB3RB4RA1RZ (bbch)	$>1.9\times 10^{704}$	Terry and Shawn Ligocki
1RB2LA4RA2LB2LA_0LA2RB3RB1RA1RZ (bbch)	$>1.6\times 10^{211}$	Terry and Shawn Ligocki
1RB2LA4RA2LB2LA_0LA2RB3RB4RA1RZ (bbch)	$>1.6\times 10^{211}$	Terry and Shawn Ligocki
1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ (bbch)	$>5.2\times 10^{61}$	Terry and Shawn Ligocki
1RB0RB4RA2LB2LA_2LA1LB3RB4RA1RZ (bbch)	$>7\times 10^{21}$	Terry and Shawn Ligocki
1RB1RZ4LA4LB2RA_2LB2RB3RB2RA0RB (bbch)	$>9\times 10^{16}$	Terry and Shawn Ligocki
1RB3LA1LA0LB1RA_2LA4LB4LA1RA1RZ (bbch)	$>3.77\times 10^{16}$	Terry and Shawn Ligocki
1RB2RA1LA3LA2RA_2LA3RB4LA1LB1RZ (bbch)	$>9\times 10^{15}$	Terry and Shawn Ligocki
1RB2RA1LA1LB3LB_2LA3RB1RZ4RA1LA (bbch)	417,310,842,648,366	Terry and Shawn Ligocki
1RB3LA1LA4LA1RA_2LB2RA1RZ0RA0RB (bbch)	26,375,397,569,930	Grégory Lafitte and Christophe Papazian
1RB3LB4LB4LA2RA_2LA1RZ3RB4RA3RB (bbch)	14,103,258,269,249	Grégory Lafitte and Christophe Papazian
1RB3RA4LB2RA3LA_2LA1RZ4RB4RB2LB (bbch)	3,793,261,759,791	Grégory Lafitte and Christophe Papazian
1RB3RA1LA1LB3LB_2LA4LB3RA2RB1RZ (bbch)	924,180,005,181	Grégory Lafitte and Christophe Papazian
1RB3LB1RZ1LA1LA_2LA3RB4LB4LB3RA (bbch)	912,594,733,606	Grégory Lafitte and Christophe Papazian
1RB2RB3LA2RA3RA_2LB2LA3LA4RB1RZ (bbch)	469,121,946,086	Grégory Lafitte and Christophe Papazian
1RB3RB3RB1LA3LB_2LA3RA4LB2RA1RZ (bbch)	233,431,192,481	Grégory Lafitte and Christophe Papazian
1RB3LA1LB1RA3RA_2LB3LA3RA4RB1RZ (bbch)	8,619,024,596	Grégory Lafitte and Christophe Papazian
1RB2RB3RB4LA3RA_0LA4RB1RZ0RB1LB (bbch)	7,543,673,517	Grégory Lafitte and Christophe Papazian

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

• 1RB2RA3LA4LA2RB_2LA3RA---0RA1LA (bbch). Chaotic via long. analysis - Notes by mxdys
• 1RB2RA3LA4LA2RB_2LA3RB---0RA1LA (bbch). Chaotic via long. analysis
• 1RB3LA1LA4LA2RA_2LB2RA---0RA0RB (bbch). - Notes by mxdys
• 1RB---4LB0LA4RA_2LB2LA3RA4LB0RB (bbch).
• 1RB4RA1LA4RB2LA_2LB3LA1RB2RA--- (bbch).
• 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA (bbch).
• 1RB2RB3LA4LA1LA_2LB3RA---4RA1RB (bbch).
• 1RB3RB3LA4LA2RB_2LB3RA---1RA1LA (bbch).
• 1RB4RB4RA1LA3LA_1LB2LA3RB2RB--- (bbch).
• 1RB2RA4LA1RB4RB_1LB2LA3RA---0LB (bbch).
• 1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- (bbch).
• 1RB3LA1LA2RB2RA_2LA4RA3LB1RA--- (bbch).
• 1RB3RB---4RA2RA_2LA2RA3LB4LB1LB (bbch).
• 1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch).
• 1RB---3LB4RB0LA_2LB3LA3RB4RA0RA (bbch).
• 1RB2LA0RB1LA3LB_1LA3LB1RA4RA--- (bbch). Shift overflow mixed-digits counter - Analysis by hipparcos
• 1RB2LA0RB4LB1RA_1LA3RA1RA---0LA (bbch). Shift overflow mixed-digits counter - Analysis by hipparcos + mxdys's notes
• 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
• 1RB3LA3LB0RB0LA_2LA4RB1LB1RA--- (bbch). Permutation of "Spaghetti TM", 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
• 1RB2LA4LA1RA1LA_2LB3RB4RB---2RA (bbch). Long. analysis rules by @Legion, ran to cell 155 without halting
• 1RB3LA1RA4LA2RA_2LA---1LA0RA3RB (bbch). Chaotic via long. analysis. More analysis by mxdys
• 1RB2RB4LA2RA1LA_2LA4RA3LA---3RA (bbch). Chaotic via long. analysis. Probviously nonhalting
• 1RB2RB---0LB3LA_2LA2LB3RB4RB1LB (bbch). Chaotic via long. analysis. Analysis of permutation by mxdys
• 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