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. Estimated 25 to 50% chance of beating champion.

Top Halters

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

Standard format	(approximate) runtime	Discoverer
1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ (bbch)	$>10^{10^{10^{3314360}}}\approx 10\uparrow \uparrow 4.8142742$	Daniel Yuan
1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA (bbch)	$>10^{38033}$	Pavel Kropitz
1RB2RA3LA4RB---_2LA3RB3RA1LB3LB (bbch)	$>6.9\times 10^{933}$	Daniel Yuan [1]
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
1RB3LA1LA2RB2LB_1LB2RA4RA0RB--- (bbch)	~ 10198	prurq
1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ (bbch)	$>5.2\times 10^{61}$	Terry and Shawn Ligocki
1RB4RA1LA4RB2LA_2LB3LA1RB2RA--- (bbch)	$>5.6\times 10^{53}$	prurq and Aristotle: proof in Lean, confirmed in Rocq
1RB3RB3LA4LA2RB_2LB3RA---1RA1LA (bbch)	$>7.3\times 10^{28}$	prurq and Aristotle: proof in Lean, confirmed in Rocq
1RB0RB4RA2LB2LA_2LA1LB3RB4RA1RZ (bbch)	$>7\times 10^{21}$	Terry and Shawn Ligocki
1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (bbch)	$>6.0\times 10^{21}$	prurq and LegionMammal978
1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch)	$>1.6\times 10^{20}$	prurq and LegionMammal978
1RB3LA4LA1LA2RA_2LA4RB---0RA0LA (bbch)	> 1020 (more accurate runtime yet to be calculated)	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

History

Timeline of bounds established for Σ(2,5) and S(2,5)
Month of discovery	Machine	S(2,5)	Σ(2,5)	Discoverer	Notes
February 2005	4RB2LA4LA4RA3LA_1LA4LA4RA3RB3LH (bbch)	≥ 16,268,767	≥ 3,685	Ligocki, T., Ligocki, S.	These bounds were published simultaneously.
	4LB1RH2RA0LB3LB_2RA3LB3RB2LB1LB (bbch)	≥ 15,754,273	≥ 4,099
April 2005	1RB4LA1LA2LA1RA_3LA1RZ1RA2RA4RB (bbch)	≥ 148,304,214	≥ 11,120
August 2005	1RB3LA1LA1RA3RA_2LB3LA3RA4RB1RZ (bbch)	≥ 8,619,024,596	≥ 90,604	Lafitte, G., Papazian, C.
September 2005	1RB2RB3RB4LA3RA_0LA4RB1RZ0RB1LB (bbch)	≥ 7,543,673,517	≥ 97,104
October 2005	1RB3RB3RB1LA3LB_2LA3RA4LB2RA1RZ (bbch)	≥ 233,431,192,481	≥ 458,357
	1RB3LB1RZ1LA1LA_2LA3RB4LB4LB3RA (bbch)	≥ 912,594,733,606	≥ 1,957,771
December 2005	1RB3RA1LA1LB3LB_2LA4LB3RA2RB1RZ (bbch)	≥ 924,180,005,181	≥ 1,137,477
May 2006	1RB3RA4LB2RA3LA_2LA2LZ4RB4RB2LB (bbch)	≥ 3,793,261,759,791	≥ 2,576,467
June 2006	1RB3LB4LB4LA2RA_2LA4LZ3RB4RA3RB (bbch)	≥ 14,103,258,269,249	≥ 4,848,239
July 2006	1RB3LA1LA4LA1RA_2LB2RA1RZ0RA0RB (bbch)	≥ 26,375,397,569,930	≥ 143
August 2006	1RB0RB4RA2LB2LA_2LA1LB3RB4RA1RZ (bbch)	≥ 7,069,449,877,176,007,352,687	≥ 172,312,766,455	Ligocki, T., Ligocki, S.
October 2007	1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ (bbch)	> 5.28 × 1061	> 9.38 × 1030
	1RB2LA4RA2LB2LA_0LA2RB3RB1RA1RZ (bbch)	> 1.67 × 10211	> 5.28 × 10105		Another functionally equivalent machine which showed the same bounds was published simultaneously.
November 2007	1RB2LA1RA2LB2LA_0LA2RB3RB4RA1RZ (bbch)	> 1.90 × 10704	> 1.78 × 10352
July 2023	1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA (bbch)	> 6.5 × 1038,033	> 7.3 × 1019,016	Kropitz, P.
June 2024	1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ (bbch)	> 1010103,314,360		Yuan, D.

Bounds highlighted in red indicate those which did not improve upon the best known at the time.

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.

Using existing C++ deciders, Andrew Ducharme found two machines non-halting on 29 Jan 2026 and 11 Feb 2026. On 11 March 2026, Peacemaker II solved a permutation of one of the TMs Andrew solved by tweaking some of the decider parameters. @mxdys verified each result the days they were announced. Also on 11 Feb 2026, @mxdys proved in Rocq another TM as a translated cycler. This combined progress reduced the formal holdout count to 71.

On 16 March 2026, mxdys formalised a proof from October 2024 and a proof from October 2025, thus reducing the holdout count to 69.^[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, then extended it the next day to solve a BMO 3 variant, reducing the holdout count to 66.

On 30 May 2026, Andrew Ducharme showed 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB (bbch) nonhalting via FAR. mxdys verified the FAR solution in Rocq on 1 June.

On 8 September 2026, mxdys used the newest Rocq deciders to solve five holdouts, leaving only 60 formal holdouts.

On 9 October 2026 prurq showed that 1RB3LA1LA2RB2LB_1LB2RA4RA0RB--- (bbch) halts in ~10¹⁹⁸ steps, using a Rocq-certified longitudinal simulator , lowering the formal holdouts count to 59.

On 3 November 2026, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of 37 holdouts.

An often up-to-date and annotated spreadsheet of holdouts, based on the June 2024 list of 217 holdouts, is available here

Holdouts

This section is based on the list of 83 holdouts published by @mxdys, and includes further progress as of 3 November 2026. All TMs with known informal arguments for halting or non-halting before that date, were formally decided, leading to the latest 37 formal holdouts list.

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 steps Analysis by legionmammal978: expected to halt in exp(exp(O(n))) steps. .
• 1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- (bbch). Does not halt in 2e13 steps.
• 1RB2RA4LA1RB4RB_1LB2LA3RA---0LB (bbch). Does not halt in 5e13 steps.
• 1RB---4LB0LA4RA_2LB2LA3RA4LB0RB (bbch).
• 1RB2RB3LA4LA1LA_2LB3RA---4RA1RB (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.
• 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). Probviously halting potential cryptid. Estimated 25 to 50% chance of beating current champion
• 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
• 1RB2LB3LA0RA1LB_2LA4RA3RB3LA--- (bbch). Analysis by @nerdyjoe
• 1RB3LB4LA0LB---_2LA0LA1RB0RA3RA (bbch). Analysis by Peacemaker II
• 1RB3RB1LB2RA---_2LA2RB1LA4LB0RA (bbch). Analysis by Legion and @dyuan
• 1RB4LA1RA1RB1LA_2LB3LA---4RA2RB (bbch). Basic long. analysis by @dyuan
• 1RB3RA3RB4LA1LA_1LB2LA1LA---1RB (bbch). Long. analysis by @dyuan suggests chaotic, potentially halt. Did not halt in ~10^17.50888 steps of simulation by Andrew Ducharme.
• 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

Solved with moderate rigor

None

Formally proven

The 22 following machines have respectively 2 halting and 20 non-halting proofs formalized in Lean by @prurq, using AI agents Aristotle (solved 4 of them, mentioned in the list) and GPT6 (solved 18 of them, with information processing and proof formalization using Aristotle). Their proofs have been confirmed in Rocq by @mxdys on 3 November 2026:

• 1RB4RA1LA4RB2LA_2LB3LA1RB2RA--- (bbch). Solved using Aristotle. Expected to halt in 5.6 x 10⁵³ steps (prurq).

• 1RB3RB3LA4LA2RB_2LB3RA---1RA1LA (bbch). Solved using Aristotle. Expected to halt in 7.3 x 10²⁸ steps (prurq). Analysis by @LegionMammal978

• 1RB3LA3LA0RB2LB_2LA4LA4RA2RA--- (bbch). Analysis by @mxdys
• 1RB3LB0RB---2LB_2LA3RA4RB2RB0LA (bbch). Analysis by @mxdys
• 1RB2LA0RB1LA3LB_1LA3LB1RA4RA--- (bbch). Shift overflow mixed-digits counter - Analysis by hipparcos
• 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).
• 1RB2LA0RB---4LA_1LA3LA1RA4RA1LB (bbch). Solved using Aristotle. Analysis by @racheline
• 1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch). Solved using Aristotle. Does not halt in 1e13 steps. Longitudinal Analysis by dyuan.
• 1RB2LA3LB4LB---_0LA4LB3RA4LA0RB (bbch). Fractal?

The 24 following machines were proven before the last 3 November 2026 release:

• 1RB3LA1LA2RB2LB_1LB2RA4RA0RB--- (bbch). Halts in ~ 10¹⁹⁸ steps (prurq), using a Rocq-certified longitudinal simulator. Block analysis by @dyuan by "impurity score"
• 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (bbch). Longitudinal analysis by @Legion implies halting, simulated until halt by prurq using Quick_Sim. Rocq-decided by @mxdys.
• 1RB3LA4LA1LA2RA_2LA4RB---0RA0LA (bbch). Longitudinal analysis by @Legion implies halting. Rocq-decided by @mxdys.
• 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (bbch). Longitudinal analysis by @Legion implies halting, simulated until halt by prurq using Quick_Sim. Rocq-decided by @mxdys.
• 1RB3RA2LB1LB1RB_2LA2RA4LA1LA--- (bbch). Dekaheptoid - Unverified nonhalting proof by @dyuan. Rocq-decided by @mxdys.
• 1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch). Dekaheptoid - Unverified nonhalting proof by @dyuan. Rocq-decided by @mxdys.

• 1RB2RA3LA4LA2RB_2LA0RA---0RA1LA (bbch). Rocq-decided by @mxdys. Longitudinal analysis by Legion implies nonhalting
• 1RB2RA3LA4RB---_2LA3RB3RA1LB3LB (bbch). Rocq-decided by @mxdys. s ~ 6.9 x 10⁹³³, halter ranked 3^rd. Halting argument by @dyuan
• 1RB3LA4RB0RB2LA_1LB2LA3LA1RA--- (bbch). Rocq-decided by @mxdys. Current champion s ~ 10^^4.81
• 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.
• 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB (bbch). Nonhalting argument by @racheline. FAR solution by Andrew Ducharme, Rocq by mxdys.