BB(2,5): Difference between revisions

Latest revision as of 02:54, 28 September 2025

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

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). Analysis by @mxdys

Top Halters

This list is incomplete. You can help by adding missing items.

Some of the longest running halting BB(2,5) TMs are:


Standard format	(approximate) runtime
`1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ` (bbch)	$10\uparrow \uparrow 4.8142742$
`1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA` (bbch)	$>10^{38\,033}$

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. 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? Basic long. analysis by @dyuan
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. More analysis by mxdys
1RB3LA3LB0RB0LA_2LA4RB1LB1RA--- (bbch).
1RB3LA1LA2RB2RA_2LA4RA3LB1RA--- (bbch).
1RB3LA3LA0RB2LB_2LA4LA4RA2RA--- (bbch). Analysis by @mxdys
1RB3RA2LB1LB1RB_2LA2RA4LA1LA—-- (bbch). Skelet 17-like
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). Analysis by @mxdys
1RB3LB4LA0LB---_2LA0LA1RB0RA3RA (bbch).
1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (bbch). Skelet 17-like
1RB3RB---4RA2RA_2LA2RA3LB4LB1LB (bbch).
1RB3RB1LB2RA---_2LA2RB1LA4LB0RA (bbch).
1RB2LA0RB1LA3LB_1LA3LB1RA4RA--- (bbch).
1RB2LA0RB4LB1RA_1LA3RA1RA---0LA (bbch).
1RB2LA0RB---4LA_1LA3LA1RA4RA1LB (bbch).
1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- (bbch).
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
1RB2LA0LB1LA2RA_0LA3RA1RA4LB—-- (bbch). Potential bouncer
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 ~9e1167 steps by @hipparcos, hasn't halted yet
1RB2LA0RB1LB---_1LA3RA1RA4LB2LB (bbch). Simulated for ~1.3e1094 steps by @hipparcos, hasn't halted yet
1RB2LA0RB1LB---_1LA3RA1RA4LB1RB (bbch). Simulated for ~9.8e1226 steps by @hipparcos, hasn't halted yet
1RB2LA0RB1LB---_1LA3RA1RA4LB1LB (bbch). Simulated for ~3.0e1140 steps by @hipparcos, hasn't halted yet
1RB2LA0RB1LB---_1LA3RA1RA4LB0RB (bbch).
1RB2LA0RB1LB---_1LA3RA1RA4LB0LB (bbch). Simulated for ~2.6e889 steps by @hipparcos, hasn't halted yet
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
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

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

@@ Line 1: / Line 1: @@
 The 2-state, 5-symbol Busy Beaver problem, '''BB(2,5)''', is unsolved. With the discovery of the [[Cryptids|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 [https://www.sligocki.com/2024/05/10/bb-2-5-is-hard.html BB(2,5) is Hard].
-The current BB(2,5) champion {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}} was discovered by Daniel Yuan in June 2024, proving the lower bounds:
+The current BB(2,5) [[Champions#5-Symbol TMs|champion]] {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}} was discovered by Daniel Yuan in June 2024, proving the lower bounds:
 <math display="block">S(2,5) > \Sigma(2,5) > 10^{10^{10^{3\,314\,360}}} > 10 \uparrow\uparrow 4</math>
@@ Line 12: / Line 12: @@
 Potential Cryptids:
-* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}
+* {{TM|1RB---0RB0LA2RA_2LB2LA3RA4LB0LB|undecided}}.
-* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}
+* {{TM|1RB3LA1LA1RA3RA_2LB2RA---4RB1LB|undecided}}.
-* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}
+* {{TM|1RB3LA1LA1RA1RA_2LB2RA---4RB1LB|undecided}}.
-* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}
+* {{TM|1RB3LB---4LA1RB_2LA4LA4LB3RB1RA|undecided}}. [https://discord.com/channels/960643023006490684/1375584513777995957 Analysis by @mxdys]
+==Top Halters==
+{{Incomplete List}}
+Some of the longest running halting BB(2,5) TMs are:
+{| class="wikitable"
+|+
+!Standard format
+!(approximate) runtime
+|-
+|{{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA1RZ|halt}}
+|<math>10 \uparrow\uparrow 4.8142742</math>
+|-
+|{{TM|1RB2LB4LB3LA1RZ_1LA3RA3LB0LB0RA|halt}}
+|<math>> 10^{38\,033}</math>
+|}
 == 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 [[Closed Tape Language (CTL)|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.
+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 lists|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 [[Closed Tape Language|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 [https://discord.com/channels/960643023006490684/1259770421046411285/1355593937531961365 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.
+On [https://discord.com/channels/960643023006490684/1259770421046411285/1355593937531961365 29 Mar 2025], @mxdys published a list of 83 holdouts that withstood state-of-the-art Rocq deciders. Some of these machines were already decided before.
 == Holdouts ==
@@ Line 56: / Line 71: @@
 * {{TM|1RB2RA3LA4LA2RB_2LA---3LB1RA3RA|undecided}}. [https://discord.com/channels/960643023006490684/1353983911222312970/1355112650690003028 Bouncer + chaotic counter]
 * {{TM|1RB2RA3LA4LA2RB_2LA3RB---0RA1LA|undecided}}. Longitudinal analysis suggests chaotic
-* {{TM|1RB3LA1RA4LA2RA_2LA---1LA0RA3RB|undecided}}. Longitudinal analysis suggests chaotic
+* {{TM|1RB3LA1RA4LA2RA_2LA---1LA0RA3RB|undecided}}. Longitudinal analysis suggests chaotic. [https://discord.com/channels/960643023006490684/1378560417235734558 More analysis by mxdys]
 * {{TM|1RB3LA3LB0RB0LA_2LA4RB1LB1RA---|undecided}}.
 * {{TM|1RB3LA1LA2RB2RA_2LA4RA3LB1RA---|undecided}}.
 * {{TM|1RB3LA3LA0RB2LB_2LA4LA4RA2RA---|undecided}}. [https://discord.com/channels/960643023006490684/1376383949575557161 Analysis by @mxdys]
 * {{TM|1RB3RA2LB1LB1RB_2LA2RA4LA1LA—--|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
-* {{TM|1RB3RA4LB2RA2RB_2LA---3LA0LB1LA|undecided}}.
 * {{TM|1RB2LB3LA0RA1LB_2LA4RA3RB3LA---|undecided}}. [https://discord.com/channels/960643023006490684/1344221797020602398/1344221797020602398 Analysis by @nerdyjoe]
 * {{TM|1RB2RB---0LB3LA_2LA2LB3RB4RB1LB|undecided}}. Longitudinal analysis suggests chaotic
@@ Line 70: / Line 84: @@
 * {{TM|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA|undecided}}. [https://discord.com/channels/960643023006490684/1084047886494470185/1244214757485973598 Skelet 17-like]
 * {{TM|1RB3RB---4RA2RA_2LA2RA3LB4LB1LB|undecided}}.
-* {{TM|1RB3RB---0RA2RB_2LA4RA3LB1LB1LA|undecided}}.
 * {{TM|1RB3RB1LB2RA---_2LA2RB1LA4LB0RA|undecided}}.
 * {{TM|1RB2LA0RB1LA3LB_1LA3LB1RA4RA---|undecided}}.
@@ Line 115: / Line 128: @@
 === Formally proven ===
-* {{TM|1RB2RA3LA4LA2RB_2LA0RA---0RA1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]
+* {{TM|1RB3RA4LB2RA2RB_2LA---3LA0LB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1411488532500971631 Rocq-decided by @mxdys.]
-* {{TM|1RB0LB2LA4LB3LA_2LA---3RA4RB2RB|undecided}}. [https://discord.com/channels/960643023006490684/1375251026411786310/1375556785603084469 Coq-decided by @mxdys]
+* {{TM|1RB3RB---0RA2RB_2LA4RA3LB1LB1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1411488532500971631 Rocq-decided by @mxdys.]
-* {{TM|1RB2LA1RA---1LA_1LA4RB3LB0RB2RB|undecided}}. [https://discord.com/channels/960643023006490684/1375251026411786310/1375556785603084469 Coq-decided by @mxdys]
+* {{TM|1RB2RA3LA4LA2RB_2LA0RA---0RA1LA|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1355828077023854752 Rocq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1355714495326060706 Longitudinal analysis by @Legion implies nonhalting]
-* {{TM|1RB2LA3LA4RA0LA_1LA3RB1RB1LB---|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379521528869421137 Coq-decided by @mxdys]
+* {{TM|1RB0LB2LA4LB3LA_2LA---3RA4RB2RB|undecided}}. [https://discord.com/channels/960643023006490684/1375251026411786310/1375556785603084469 Rocq-decided by @mxdys]
-* {{TM|1RB2RA3LA4RB---_2LA3RB3RA1LB3LB|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Coq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1373347187836194898 Halting argument by @dyuan]
+* {{TM|1RB2LA1RA---1LA_1LA4RB3LB0RB2RB|undecided}}. [https://discord.com/channels/960643023006490684/1375251026411786310/1375556785603084469 Rocq-decided by @mxdys]
-* {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Coq-decided by @mxdys]. Current champion
+* {{TM|1RB2LA3LA4RA0LA_1LA3RB1RB1LB---|undecided}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379521528869421137 Rocq-decided by @mxdys]
+* {{TM|1RB2RA3LA4RB---_2LA3RB3RA1LB3LB|halt}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Rocq-decided by @mxdys]. [https://discord.com/channels/960643023006490684/1259770421046411285/1373347187836194898 Halting argument by @dyuan]
+* {{TM|1RB3LA4RB0RB2LA_1LB2LA3LA1RA---|halt}}. [https://discord.com/channels/960643023006490684/1259770421046411285/1379877629288644722 Rocq-decided by @mxdys]. Current champion
-[[Category:BB Domain]]
+[[Category:BB Domains]][[Category:BB(2,5)]]

BB(2,5): Difference between revisions

Latest revision as of 02:54, 28 September 2025

Contents

Cryptids

Top Halters

Certified progress

Holdouts

Cryptids

Unsolved

Solved with moderate rigor

Formally proven

Navigation menu