BB(2,5): Difference between revisions

Latest revision as of 12:55, 3 November 2026

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) > Σ (2, 5) > 1 0^{1 0^{1 0^{3 314 360}}} > 10 ↑ ↑ 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)	$> 1 0^{1 0^{1 0^{3 314 360}}} \approx 10 ↑ ↑ 4.8142742$	Daniel Yuan
`1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA` (bbch)	$> 1 0^{38 033}$	Pavel Kropitz
`1RB2RA3LA4RB---_2LA3RB3RA1LB3LB` (bbch)	$> 6.9 \times 1 0^{933}$	Daniel Yuan [1]
`1RB2LA1RA2LB2LA_0LA2RB3RB4RA1RZ` (bbch)	$> 1.9 \times 1 0^{704}$	Terry and Shawn Ligocki
`1RB2LA4RA2LB2LA_0LA2RB3RB1RA1RZ` (bbch)	$> 1.6 \times 1 0^{211}$	Terry and Shawn Ligocki
`1RB2LA4RA2LB2LA_0LA2RB3RB4RA1RZ` (bbch)	$> 1.6 \times 1 0^{211}$	Terry and Shawn Ligocki
`1RB3LA1LA2RB2LB_1LB2RA4RA0RB---` (bbch)	~ 10¹⁹⁸	prurq
`1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ` (bbch)	$> 5.2 \times 1 0^{61}$	Terry and Shawn Ligocki
`1RB4RA1LA4RB2LA_2LB3LA1RB2RA---` (bbch)	$> 5.6 \times 1 0^{53}$	prurq and Aristotle: proof in Lean, confirmed in Rocq
`1RB3RB3LA4LA2RB_2LB3RA---1RA1LA` (bbch)	$> 7.3 \times 1 0^{28}$	prurq and Aristotle: proof in Lean, confirmed in Rocq
`1RB0RB4RA2LB2LA_2LA1LB3RB4RA1RZ` (bbch)	$> 7 \times 1 0^{21}$	Terry and Shawn Ligocki
`1RB2RA3LA4LA2RB_2LA---1LA1RA3RA` (bbch)	$> 6.0 \times 1 0^{21}$	prurq and LegionMammal978
`1RB3LA4LA2RB1LA_2LA4RB---3RA3LA` (bbch)	$> 1.6 \times 1 0^{20}$	prurq and LegionMammal978
`1RB3LA4LA1LA2RA_2LA4RB---0RA0LA` (bbch)	> 10²⁰ (more accurate runtime yet to be calculated)	LegionMammal978
`1RB1RZ4LA4LB2RA_2LB2RB3RB2RA0RB` (bbch)	$> 9 \times 1 0^{16}$	Terry and Shawn Ligocki
`1RB3LA1LA0LB1RA_2LA4LB4LA1RA1RZ` (bbch)	$> 3.77 \times 1 0^{16}$	Terry and Shawn Ligocki
`1RB2RA1LA3LA2RA_2LA3RB4LA1LB1RZ` (bbch)	$> 9 \times 1 0^{15}$	Terry and Shawn Ligocki
`1RB2LB4RB2RB---_1LA3RA4RA3LB1LB` (bbch)	$6.64187 \times 1 0^{15}$	mxdys
`1RB2RB4LB2LB---_2LA0LA3RB0LA2RA` (bbch)	$3.1317 \times 1 0^{15}$	mxdys
`1RB0RA3LB1LB---_2LA3RB4RB3RA0LA` (bbch)	$2.7527 \times 1 0^{15}$	mxdys

History

Timeline of bounds established for Σ(2,5) and S(2,5)^[1]
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.^[2]	These bounds were published simultaneously.
February 2005	`4LB1RH2RA0LB3LB_2RA3LB3RB2LB1LB` (bbch)	≥ 15,754,273	≥ 4,099		These bounds were published simultaneously.
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.^[2]
September 2005	`1RB2RB3RB4LA3RA_0LA4RB1RZ0RB1LB` (bbch)	≥ 7,543,673,517	≥ 97,104
October 2005	`1RB3RB3RB1LA3LB_2LA3RA4LB2RA1RZ` (bbch)	≥ 233,431,192,481	≥ 458,357
October 2005	`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.^[2]
October 2007	`1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ` (bbch)	> 5.28 × 10⁶¹	> 9.38 × 10³⁰
October 2007	`1RB2LA4RA2LB2LA_0LA2RB3RB1RA1RZ` (bbch)	> 1.67 × 10²¹¹	> 5.28 × 10¹⁰⁵		Another functionally equivalent machine which showed the same bounds was published simultaneously.
November 2007	`1RB2LA1RA2LB2LA_0LA2RB3RB4RA1RZ` (bbch)	> 1.90 × 10⁷⁰⁴	> 1.78 × 10³⁵²
July 2023	`1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA` (bbch)	> 6.5 × 10^38,033	> 7.3 × 10^19,016	Kropitz, P.
June 2024	`1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ` (bbch)	> 10^{10^{10^3,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 * 1 0^{1167}$ steps by @hipparcos, hasn't halted yet
- 1RB2LA0RB1LB---_1LA3RA1RA4LB2LB (bbch). Simulated for $1.3 * 1 0^{1094}$ steps by @hipparcos, hasn't halted yet
- 1RB2LA0RB1LB---_1LA3RA1RA4LB1RB (bbch). Simulated for $9.8 * 1 0^{1226}$ steps by @hipparcos, hasn't halted yet
- 1RB2LA0RB1LB---_1LA3RA1RA4LB1LB (bbch). Simulated for $3 * 1 0^{1140}$ steps by @hipparcos, hasn't halted yet
- 1RB2LA0RB1LB---_1LA3RA1RA4LB0LB (bbch). Simulated for $2.6 * 1 0^{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.

References

↑ Pascal Michel. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62
↑ ^2.0 ^2.1 ^2.2 https://web.archive.org/web/20160420171959/http://www.drb.insel.de/~heiner/BB/bbsimtab.html

[:PMH-1] Pascal Michel. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62

[:0-2] 2.0 ^2.1 ^2.2 https://web.archive.org/web/20160420171959/http://www.drb.insel.de/~heiner/BB/bbsimtab.html

[1]

[2]

@@ Line 49: / Line 49: @@
 |<math>>1.6 \times 10^{211}</math>
 |Terry and Shawn Ligocki
+|-
+|{{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}
+|~ 10<sup>198</sup>
+|[https://discord.com/channels/960643023006490684/1259770421046411285/1558226290509742082 prurq]
 |-
 |{{TM|1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ|halt}}
 |<math>>5.2 \times 10^{61}</math>
 |Terry and Shawn Ligocki
+|-
+|{{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|halt}}
+|<math>>5.6 \times 10^{53}</math>
+|prurq and Aristotle: proof in Lean, confirmed in Rocq
+|-
+|{{TM|1RB3RB3LA4LA2RB_2LB3RA---1RA1LA|halt}}
+|<math>>7.3 \times 10^{28}</math>
+|prurq and Aristotle: proof in Lean, confirmed in Rocq
 |-
 |{{TM|1RB0RB4RA2LB2LA_2LA1LB3RB4RA1RZ|halt}}
@@ Line 93: / Line 105: @@
 |<math>2.7527 \times 10^{15}</math>
 |mxdys
-|-
-|{{TM|1RB2LB2RA4LB1RA_1LA3RA3LA4LA---|halt}}
-|<math>1.7828 \times 10^{15}</math>
-|mxdys
-|-
-|{{TM|1RB3LA---4RB0LB_2LA3LB4LA1RB3RA|halt}}
-|<math>6.66046 \times 10^{14}</math>
-|mxdys
-|-
-|{{TM|1RB2RA1LA1LB3LB_2LA3RB1RZ4RA1LA|halt}}
-|417,310,842,648,366
-|Terry and Shawn Ligocki
 |}
 == History ==
 {| class="wikitable mw-collapsible"
-! colspan="6" |Timeline of lower bounds established for Σ(2,5) and S(2,5)<ref name=":PMH">Pascal Michel. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62</ref>
+! colspan="6" |Timeline of bounds established for Σ(2,5) and S(2,5)<ref name=":PMH">Pascal Michel. (last updated 2026). The Busy Beaver Competition: a historical survey. https://bbchallenge.org/~pascal.michel/ha#tm62</ref>
 |-
 !Month of discovery
 !Machine
-!S(2,5) lower bound
+!S(2,5)
-!Σ(2,5) lower bound
+!Σ(2,5)
 !Discoverer
 !Notes
@@ Line 121: / Line 121: @@
 |{{TM|4RB2LA4LA4RA3LA_1LA4LA4RA3RB3LH|halt}}
 |≥ 16,268,767
-|(≥ 3,685)
+| style="background: #FFCCCC;" |≥ 3,685
-| rowspan="3" |Ligocki, T., Ligocki, S.
+| rowspan="3" |Ligocki, T., Ligocki, S.<ref name=":0">https://web.archive.org/web/20160420171959/http://www.drb.insel.de/~heiner/BB/bbsimtab.html</ref>
-| rowspan="2" |During this period, the steps champion was different to the ones champion.
+| rowspan="2" |These bounds were published simultaneously.
-These bounds were published simultaneously.
 |-
 |{{TM|4LB1RH2RA0LB3LB_2RA3LB3RB2LB1LB|halt}}
-|(≥ 15,754,273)
+| style="background: #FFCCCC;" |≥ 15,754,273
 |≥ 4,099
 |-
@@ Line 140: / Line 139: @@
 |≥ 8,619,024,596
 |≥ 90,604
-| rowspan="8" |Lafitte, G., Papazian, C.
+| rowspan="8" |Lafitte, G., Papazian,&nbsp;C.<ref name=":0" />
 |
 |-
-|September 2005
+|September&nbsp;2005
 |{{TM|1RB2RB3RB4LA3RA_0LA4RB1RZ0RB1LB|halt}}
-|(≥ 7,543,673,517)
+| style="background: #FFCCCC;" |≥ 7,543,673,517
 |≥ 97,104
-|During this period, the steps champion was different to the ones champion.
+|
 |-
 | rowspan="2" |October 2005
@@ Line 163: / Line 162: @@
 |{{TM|1RB3RA1LA1LB3LB_2LA4LB3RA2RB1RZ|halt}}
 |≥ 924,180,005,181
-|(≥ 1,137,477)
+| style="background: #FFCCCC;" |≥ 1,137,477
-|During this period, the steps champion was different to the ones champion.
+|
 |-
 |May 2006
@@ Line 181: / Line 180: @@
 |{{TM|1RB3LA1LA4LA1RA_2LB2RA1RZ0RA0RB|halt}}
 |≥ 26,375,397,569,930
-|(≥ 143)
+| style="background: #FFCCCC;" |≥ 143
-|During this period, the steps champion was different to the ones champion.
+|
 |-
 |August 2006
 |{{TM|1RB0RB4RA2LB2LA_2LA1LB3RB4RA1RZ|halt}}
-|≥ 7,069,449,877,176,007,352,687
+|≥&nbsp;7,069,449,877,176,007,352,687
-|≥ 172,312,766,455
+|≥&nbsp;172,312,766,455
-| rowspan="4" |Ligocki, T., Ligocki, S.
+| rowspan="4" |Ligocki, T., Ligocki, S.<ref name=":0" />
 |
 |-
 | rowspan="2" |October 2007
 |{{TM|1RB2LA4RA1LB2LA_0LA2RB3RB2RA1RZ|halt}}
-|> 5.2 × 10<sup>61</sup>
+|> 5.28 × 10<sup>61</sup>
-|> 9.3 × 10<sup>30</sup>
+|> 9.38 × 10<sup>30</sup>
 |
 |-
 |{{TM|1RB2LA4RA2LB2LA_0LA2RB3RB1RA1RZ|halt}}
-|> 1.6 × 10<sup>211</sup>
+|> 1.67 × 10<sup>211</sup>
-|> 5.2 × 10<sup>105</sup>
+|> 5.28 × 10<sup>105</sup>
 |Another functionally equivalent machine which showed the same bounds was published simultaneously.
 |-
 |November 2007
 |{{TM|1RB2LA1RA2LB2LA_0LA2RB3RB4RA1RZ|halt}}
-|> 1.9 × 10<sup>704</sup>
+|> 1.90 × 10<sup>704</sup>
-|> 1.7 × 10<sup>352</sup>
+|> 1.78 × 10<sup>352</sup>
 |
 |-
@@ Line 220: / Line 219: @@
 |Yuan, D.
 |
 |}
+Bounds highlighted in <span style="background: #FFCCCC">red</span> indicate those which did not improve upon the best known at the time.
 === Certified progress ===
@@ Line 236: / Line 236: @@
 On [https://discord.com/channels/960643023006490684/1259770421046411285/1546880921318326282 8 September 2026], mxdys used the newest Rocq deciders to solve five holdouts, leaving only 60 formal holdouts.
+On [https://discord.com/channels/960643023006490684/1259770421046411285/1558226290509742082 9 October 2026] prurq showed that {{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}} halts in ~10<sup>198</sup> steps, using a [https://discord.com/channels/960643023006490684/1259770421046411285/1560264094760575088 Rocq-certified longitudinal simulator] , lowering the formal holdouts count to 59.
+On [https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584 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 [https://docs.google.com/spreadsheets/d/1qiZ3PJb_q4j9kddm0zZMionJhYCI_uEHr1bSmsBOlZs/edit?usp=drivesdk here]
 == Holdouts ==
-The number of holdouts as of Oct.1, 2026 is 60 as Rocq-proven, of which 21 have been informally solved, 39 holdouts remain including Cryptids and unsolved TMs.
+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.
-This section is based on the list of 83 holdouts published by @mxdys, and includes further progress past 8 September 2026. All TMs with known informal arguments for halting or non-halting before that date, were formally decided.
 === Cryptids ===
@@ Line 253: / Line 255: @@
 * {{TM|1RB2RA3LA4LA2RB_2LA3RA---0RA1LA|undecided}}. Chaotic via [[Longitudinal Analysis|long. analysis]] - [https://discord.com/channels/960643023006490684/1259770421046411285/1436149296004071615 Notes by mxdys]
 * {{TM|1RB2RA3LA4LA2RB_2LA3RB---0RA1LA|undecided}}. Chaotic via long. analysis
-* {{TM|1RB---3RA2LA2RB_2LB3LA4LB4RA0RA|undecided}}. [https://discord.com/channels/960643023006490684/1471178503235043493/1471206925096980664 Does not halt in 1.25e13]
+* {{TM|1RB---3RA2LA2RB_2LB3LA4LB4RA0RA|undecided}}. [https://discord.com/channels/960643023006490684/1471178503235043493/1471206925096980664 Does not halt in 1.25e13 steps]  [https://discord.com/channels/960643023006490684/1259770421046411285/1559400536690794496 Analysis by legionmammal978: expected to halt in exp(exp(O(n))) steps.]  .
 * {{TM|1RB3RB1LA2LA3RA_1LB2RA4RB0LA---|undecided}}. [https://discord.com/channels/960643023006490684/1471178503235043493/1471178503235043493 Does not halt in 2e13 steps.]
 * {{TM|1RB2RA4LA1RB4RB_1LB2LA3RA---0LB|undecided}}. [https://discord.com/channels/960643023006490684/1471178503235043493/1471206925096980664 Does not halt in 5e13 steps.]
 * {{TM|1RB---4LB0LA4RA_2LB2LA3RA4LB0RB|undecided}}.
-* {{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|undecided}}.
 * {{TM|1RB2RB3LA4LA1LA_2LB3RA---4RA1RB|undecided}}.
 * {{TM|1RB---3LB4RB0LA_2LB3LA3RB4RA0RA|undecided}}.
@@ Line 269: / Line 270: @@
 * {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}. Potential Cryptid - [https://discord.com/channels/960643023006490684/1354037062830919690/1354037062830919690 Shift overflow counter]
 * {{TM|1RB2RA3LB---2LB_2LA0LA4RB0RB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329808777754706046 Probviously halting potential cryptid. Estimated 25 to 50% chance of beating current champion]
-* {{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}. [https://discord.com/channels/960643023006490684/1395820706050080869/1395820706050080869 Block analysis by @dyuan by "impurity score"]
 * {{TM|1RB---4LB1RA4RA_2LB2LA3RA4LB0RB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1378248683161653289 Analysis by Andrew Ducharme and @mxdys]
 * {{TM|1RB---4RB2RB4LA_2LB3LA3LB0RA0RB|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1353983911222312970 Bouncer + chaotic counter]
@@ Line 281: / Line 281: @@
 * {{TM|1RB3RB1LB2RA---_2LA2RB1LA4LB0RA|undecided}}. [https://discord.com/channels/960643023006490684/1397318518961082398 Analysis by Legion and @dyuan]
 * {{TM|1RB4LA1RA1RB1LA_2LB3LA---4RA2RB|undecided}}. [https://discord.com/channels/960643023006490684/1359561443929886760 Basic long. analysis by @dyuan]
-* {{TM|1RB3RA3RB4LA1LA_1LB2LA1LA---1RB|undecided}}. [https://discord.com/channels/960643023006490684/1349602897024782358 Long. analysis by @dyuan suggests chaotic, potentially halt]
+* {{TM|1RB3RA3RB4LA1LA_1LB2LA1LA---1RB|undecided}}. [https://discord.com/channels/960643023006490684/1349602897024782358 Long. analysis by @dyuan suggests chaotic, potentially halt]. Did not halt in ~10^17.50888 steps of simulation by Andrew Ducharme.
 * {{TM|1RB2LA4LA1RA1LA_2LB3RB4RB---2RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1255570421437169805 Long. analysis rules by @Legion, ran to cell 155 without halting]
 * {{TM|1RB2RB4LA2RA1LA_2LA4RA3LA---3RA|undecided}}. Chaotic via long. analysis. [https://discord.com/channels/960643023006490684/1353983911222312970/1353987502062702622 Probviously nonhalting]
@@ Line 289: / Line 289: @@
 * {{TM|1RB2LA3LA4RA1LA_0LA3LB3RB1RB---|undecided}}. 1D CA-like
 === Solved with moderate rigor ===
-The 21 following machines have respectively 1 halting and 20 non-halting proofs formalized in Lean by @prurq, using AI agents Aristotle (solved 3 of them, mentioned in the list) and GPT6 (solved 18 of them, with information processing and proof formalization using Aristotle); however their proofs have not been independently verified:
+''None''
+=== Formally proven ===
+The 22 following machines have respectively 2 halting and 20 non-halting proofs formalized in Lean by [https://discord.com/channels/960643023006490684/1259770421046411285/1552990521650319453 @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 [https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584 3 November 2026]:
+*{{TM|1RB4RA1LA4RB2LA_2LB3LA1RB2RA---|undecided}}. Solved using Aristotle. Expected to halt in 5.6 x 10<sup>53</sup> steps [https://discord.com/channels/960643023006490684/1259770421046411285/1555690509245087827 (prurq)].
 * {{TM|1RB3RB3LA4LA2RB_2LB3RA---1RA1LA|undecided}}. Solved using Aristotle. Expected to halt in 7.3 x 10<sup>28</sup> steps [https://discord.com/channels/960643023006490684/1259770421046411285/1553433274762919997 (prurq)]. [https://discord.com/channels/960643023006490684/1259770421046411285/1498450794582900878 Analysis by @LegionMammal978]
@@ Line 313: / Line 317: @@
 * {{TM|1RB2LA0RB---4LA_1LA3LA1RA4RA1LB|undecided}}. Solved using Aristotle. [https://discord.com/channels/960643023006490684/1259770421046411285/1329629220795715674 Analysis by @racheline]
 * {{TM|1RB2LA0RB4LB0LA_1LA3LA1RA4RA---|undecided}}. Solved using Aristotle. [https://discord.com/channels/960643023006490684/1471178503235043493/1471206925096980664 Does not halt in 1e13 steps.] [https://discord.com/channels/960643023006490684/1489363702560849920/1489363702560849920 Longitudinal Analysis by dyuan.]
 * {{TM|1RB2LA3LB4LB---_0LA4LB3RA4LA0RB|undecided}}. Fractal?
-=== Formally proven ===
+The 24 following machines were proven before the last 3 November 2026 release:
+*{{TM|1RB3LA1LA2RB2LB_1LB2RA4RA0RB---|undecided}}. Halts in ~ 10<sup>198</sup> steps [https://discord.com/channels/960643023006490684/1259770421046411285/1558226290509742082 (prurq)], using a [https://discord.com/channels/960643023006490684/1259770421046411285/1560264094760575088 Rocq-certified longitudinal simulator]. [https://discord.com/channels/960643023006490684/1395820706050080869/1395820706050080869 Block analysis by @dyuan by "impurity score"]
 *{{TM|1RB2RA3LA4LA2RB_2LA---1LA1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting], [https://discord.com/channels/960643023006490684/1259770421046411285/1492999358482874448 simulated until halt by prurq using Quick_Sim]. [https://discord.com/channels/960643023006490684/1259770421046411285/1546880921318326282 Rocq-decided by @mxdys.]
 * {{TM|1RB3LA4LA1LA2RA_2LA4RB---0RA0LA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 Longitudinal analysis by @Legion implies halting]. [https://discord.com/channels/960643023006490684/1259770421046411285/1546880921318326282 Rocq-decided by @mxdys.]
@@ Line 341: / Line 345: @@
 * {{TM|1RB0RA3LA4LA2RA_2LB3LA---4RA3RB|undecided}}. BMO problem 3 variant - [https://discord.com/channels/960643023006490684/1259770421046411285/1415337575543214132 Nonhalting argument by @dyuan], [https://discord.com/channels/960643023006490684/1259770421046411285/1489095097373954199 translated to Rocq by @mxdys] using an LLM.
 * {{TM|1RB2LB---4LB0RB_1LA3RB4RB4RA1LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Nonhalting argument by @racheline]. [https://discord.com/channels/960643023006490684/1259770421046411285/1510322250769760376 FAR solution by Andrew Ducharme], [https://discord.com/channels/960643023006490684/1259770421046411285/1510867717194911874 Rocq by mxdys.]
+== References ==
 [[Category:BB Domains]][[Category:BB(2,5)]]

BB(2,5): Difference between revisions

Latest revision as of 12:55, 3 November 2026

Contents

Cryptids

Top Halters

History

Certified progress

Holdouts

Cryptids

Unsolved

Solved with moderate rigor

Formally proven

References

Navigation menu

BB(2,5): Difference between revisions

Latest revision as of 12:55, 3 November 2026

Cryptids

Top Halters

History

Certified progress

Holdouts

Cryptids

Unsolved

Solved with moderate rigor

Formally proven

References

Navigation menu

Search