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
1RB2RA3LA4RB---_2LA3RB3RA1LB3LB (bbch)	$>8.3\times 10^{466}$ (lower bound given by score)	Daniel Yuan
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
1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (bbch)	$>6.04\times 10^{21}$	prurq and LegionMammal978
1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch)	$>1.589\times 10^{20}$	prurq and LegionMammal978
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
1RB2LB4RB2RB---_1LA3RA4RA3LB1LB (bbch)	$6.64187\times 10^{15}$	mxdys
1RB2RB4LB2LB---_2LA0LA3RB0LA2RA (bbch)	$3.1317\times 10^{15}$	mxdys
1RB0RA3LB1LB---_2LA3RB4RB3RA0LA (bbch)	$2.7527\times 10^{15}$	mxdys
1RB2LB2RA4LB1RA_1LA3RA3LA4LA--- (bbch)	$1.7828\times 10^{15}$	mxdys
1RB3LA---4RB0LB_2LA3LB4LA1RB3RA (bbch)	$6.66046\times 10^{14}$	mxdys
1RB2RA1LA1LB3LB_2LA3RB1RZ4RA1LA (bbch)	417,310,842,648,366	Terry and Shawn Ligocki
1RB3LA1LA2LA1RA_2LB3RA2RB4RB--- (bbch)	$1.61577\times 10^{14}$	mxdys

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^{[1][2][3][4][5]}, lowering the certified holdout count to 75. There are 11 informal arguments, lowering the informal holdout count to 64.

Then, on 29 Jan 2026, Andrew Ducharme found a machine nonhalting. This was verified by @mxdys the same day. Hence the certified holdout count is 74, and there are still 11 informal arguments, with the informal holdout count being 63.

Later, on 11 Feb 2026, Andrew Ducharme found another machine nonhalting, again verified by @mxdys the same day. @mxdys also announced another TM as a translated cycler, thus reducing the holdout count to 72, with 61 informal holdouts.

On 11 March 2026, Peacemaker II solved a permutation of one of the TMs Andrew solved by tweaking some of the decider parameters. This result was verified by @mxdys the same day, reducing the holdout count to 71, with 60 informal holdouts.

On 16 March 2026, mxdys formalised a proof from October 2024 and a proof from October 2025, thus reducing the holdout count to 69, with 60 informal holdouts.^[6][7]

On 1 April 2026, Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution, which he created using Aristotle AI. Then mxdys formalised the result in Rocq using LLMs, reducing the holdout count to 67, with 60 informal holdouts.

On 2 April 2026, mxdys formalised BMO 3 variant 1RB0RA3LA4LA2RA_2LB3LA---4RA3RB (bbch) using an LLM, reducing the formal holdout count to 66. The proofs for BMO 3 and its variant are available at https://github.com/ccz181078/busycoq/blob/BB6/verify/BMO3.v.

Holdouts

This section is based on the list of 83 holdouts published by @mxdys, and includes further progress as of 10 April 2026. There are 66 Rocq-holdouts, or 60 when considering informal proofs.

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
• 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA (bbch). Does not halt in 1.25e13
• 1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- (bbch). Does not halt in 2e13 steps.
• 1RB2RA4LA1RB4RB_1LB2LA3RA---0LB (bbch). Does not halt in 5e13 steps.
• 1RB---4LB0LA4RA_2LB2LA3RA4LB0RB (bbch).
• 1RB4RA1LA4RB2LA_2LB3LA1RB2RA--- (bbch).
• 1RB2RB3LA4LA1LA_2LB3RA---4RA1RB (bbch).
• 1RB3RB3LA4LA2RB_2LB3RA---1RA1LA (bbch).
• 1RB---3LB4RB0LA_2LB3LA3RB4RA0RA (bbch).
• 1RB3RB---4RA2RA_2LA2RA3LB4LB1LB (bbch). Longitudinal Analysis by dyuan.
• 1RB3LA1LA2RB2RA_2LA4RA3LB1RA--- (bbch). Longitudinal Analysis by dyuan.
• 1RB4RB4RA1LA3LA_1LB2LA3RB2RB--- (bbch). Longitudinal Analysis by dyuan.
• 1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch). Does not halt in 1e13 steps. Longitudinal Analysis by dyuan.
• 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, does not halt in 4e13.
• 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
• 1RB2RB4LA2RA1LA_2LA4RA3LA---3RA (bbch). Chaotic via long. analysis. Probviously nonhalting
• 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?

14 grandchildren of 1RB2LA0RB1LB_1LA3RA1RA--- (bbch)

• 1RB2LA0RB1LB---_1LA3RA1RA4RB0LB (bbch).

and 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

• 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (bbch). Longitudinal analysis by @Legion implies halting, simulated until halt by prurq using Quick_Sim
• 1RB3LA4LA1LA2RA_2LA4RB---0RA0LA (bbch). Longitudinal analysis by @Legion implies halting
• 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch). Longitudinal analysis by @Legion implies halting, simulated until halt by prurq using Quick_Sim
• 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB (bbch). Nonhalting argument by @racheline
• 1RB3RA2LB1LB1RB_2LA2RA4LA1LA--- (bbch). Dekaheptoid - Unverified nonhalting proof by @dyuan
• 1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch). Dekaheptoid - Unverified nonhalting proof 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
• 1RB2LA0LB1LA2RA_0LA3RA1RA4LB--- (bbch). Nonhalting argument by Peacemaker II. Confirmed in Rocq by @mxdys.
• 1RB2LA1RA---1LA_1LA4RB3LB0RB2RB (bbch). Rocq-decided by @mxdys
• 1RB2LA3LA4RA0LA_1LA3RB1RB1LB--- (bbch). Rocq-decided by @mxdys
• 1RB2LA0RB1LB0LB_1LA3RA1RA4RA--- (bbch). Non-halting found by Andrew Ducharme. Confirmed in Rocq by @mxdys. Grandchild of 1RB2LA0RB1LB_1LA3RA1RA--- (bbch).
• 1RB2RB---0LB3LA_2LA2LB3RB4RB1LB (bbch). Chaotic via long. analysis. Analysis of permutation by mxdys. Non-halting found by Andrew Ducharme. Confirmed in Rocq by @mxdys.
• 1RB3LA1RA4LA2RA_2LA---1LA0RA3RB (bbch). Chaotic via long. analysis. More analysis by mxdys. High-level behaviour by Peacemaker II. Non-halting found by Peacemaker II. Confirmed in Rocq by @mxdys.
• 1RB3LA1LA4LA2RA_2LB2RA---0RA0RB (bbch). - Notes by @mxdys. Translated cycler via @mxdys.
• 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA (bbch). Nonhalting argument by @dyuan. Confirmed in Rocq by @mxdys.
• 1RB1RB3LA4LA2RA_2LB3RA---3RA4RB (bbch). BMO problem 3 by @dyuan. Confirmed in Lean by @mammillaria using Aristotle AI, translated to Rocq by @mxdys using other LLM.
• 1RB0RB3LA4LA2RA_2LB3RA---3RA4RB (bbch). BMO problem 3 by @dyuan. Confirmed in Lean by @mammillaria using Aristotle AI, translated to Rocq by @mxdys using other LLM.
• 1RB0RA3LA4LA2RA_2LB3LA---4RA3RB (bbch). BMO problem 3 variant - Nonhalting argument by @dyuan, translated to Rocq by @mxdys using an LLM.