BB(3,3): Difference between revisions
m (→Holdouts: formatting changes) |
No edit summary |
||
Line 1: | Line 1: | ||
The 3-state, 3-symbol Busy Beaver problem '''BB(3,3)''' is unsolved. With the discovery of [[Bigfoot]] in 2023, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(3,3) and thus [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3,3) is Hard]. | The 3-state, 3-symbol Busy Beaver problem '''BB(3,3)''' is unsolved. With the discovery of the [[Cryptids|Cryptid]] [[Bigfoot]] in 2023, we now know that we must solve a [[Collatz-like]] problem in order to solve BB(3,3) and thus [https://www.sligocki.com/2023/10/16/bb-3-3-is-hard.html BB(3,3) is Hard]. | ||
The current BB(3,3) champion {{TM|0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC|halt}} was discovered by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in 2007, proving the lower bounds: | The current BB(3,3) champion {{TM|0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC|halt}} was discovered by [[User:tjligocki|Terry]] and [[User:sligocki|Shawn Ligocki]] in 2007, proving the lower bounds: |
Revision as of 16:10, 20 January 2025
The 3-state, 3-symbol Busy Beaver problem BB(3,3) is unsolved. With the discovery of the Cryptid Bigfoot in 2023, we now know that we must solve a Collatz-like problem in order to solve BB(3,3) and thus BB(3,3) is Hard.
The current BB(3,3) champion 0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC
(bbch) was discovered by Terry and Shawn Ligocki in 2007, proving the lower bounds:
On bbchallenge.org Discord we have reduced the unofficial holdouts list to 22 TMs. One of these, 1RB2LC1RC_2LC---2RB_2LA0LB0RA
(bbch), is under very active exploration in channel #bb3x3 and believed to be a probviously halting TM by some members. If it halts, it will be the new champion.
Cryptids
Known BB(3,3) Cryptids:
1RB2RA1LC_2LC1RB2RB_---2LA1LA
(bbch), known as Bigfoot
Possibly probviously halting Cryptid:
Top Halters
The current top 10 BB(3,3) halters (known by Shawn Ligocki) are
0RB2LA1RA_1LA2RB1RC_1RZ1LB1LC Halt 119112334170342541 374676383 1RB2LA1LC_0LA2RB1LB_1RZ1RA1RC Halt 119112334170342540 374676383 1RB2RC1LA_2LA1RB1RZ_2RB2RA1LC Halt 4345166620336565 95524079 1RB1LA2LC_2LA2RB1RB_1RZ0LB0RC Halt 452196003014837 21264944 1RB1RZ2LC_1LC2RB1LB_1LA2RC2LA Halt 4144465135614 2950149 1RB2LA1RA_1RC2RB0RC_1LA1RZ1LA Halt 987522842126 1525688 1RB1RZ2RB_1LC0LB1RA_1RA2LC1RC Halt 4939345068 107900 1RB2LA1RA_1LB1LA2RC_1RZ1LC2RB Halt 1808669066 43925 1RB2LA1RA_1LC1LA2RC_1RZ1LA2RB Halt 1808669046 43925 1RB2LA1RA_1LB1LA2RC_1RZ1LA2RB Halt 1808669046 43925
Numbers listed are step count and sigma score for each TM. For a longer list of halting TMs see https://github.com/sligocki/busy-beaver/blob/main/Machines/bb/3x3. For historical perspective see Pascal Michel's Historical survey of Busy Beavers.
Certified Progress
On 5 Jan 2025, @tligocki finished an enumeration and filtering of the BB(3,3) machines using the established Ligocki filters, listing the filter used for each machine. He also computed the number of steps and sigma scores for all found halting TMs. The thorough results are located here. 367 machines remained on that list.
Over two-thirds of the 367 remaining machines were shown to be non-halting with FAR and MITMWFAR by @Justin Blanchard on 14 July 2024.
Most of the remainders were shown non-halting by @lijil on 8 June 2023.
These leaves 21 TMs, very similar to the more informal list identified below. The odd one out in the list below is 1RB2LA0LA_2LC---2RA_0RA2RC1LC
(bbch), which is on @lijil's certified list.
Holdouts
@Justin Blanchard's informal holdouts list is down to 22 TMs as of 9 Jun 2024. @Andrew Ducharme has categorized them as follows:
Cryptids
- 829: Bigfoot:
1RB2RA1LC_2LC1RB2RB_---2LA1LA
(bbch)
Unsolved:
1RB1LB2LC_1LA2RB1RB_---0LA2LA
(bbch) (397)- Group 2
1RB0LB0RC_2LC2LA1RA_1RA1LC---
(bbch) (153, equivalent to 758)1RB2LC1RC_2LC---2RB_2LA0LB0RA
(bbch) (758, equivalent to 153)
- Group 3
1RB2LA1LA_2LA0RA2RC_---0LC2RA
(bbch) (531, equivalent to 532)1RB2LA1LA_2LA0RA2RC_---1RB2RA
(bbch) (532, equivalent to 531)
Non-halting TMs with solutions/proofs of varying rigorousness:
- Group 1 (Discord summary of proofs)
1RB---0LC_2LC2RC1LB_0RA2RB0LB
(bbch) (21, equivalent to 92 and 818). Longitudinal analysis by @Legion implies non-halting.1RB---1RB_2LC2RC1LB_0RA2RB0LB
(bbch) (92, equivalent to 21 and 818). Equivalence claim to 21 by @dyuan1.1RB2LC---_0LA0RC1LC_1RB2RC1LB
(bbch) (683)1RB2RA1LB_0LC0RA1LA_---2LA---
(bbch) (816). See discussion of likely non-halting by @Rae and @Peacemaker on 28 August 2024.1RB2RA1LB_0LC0RA1LA_---2RB2LA
(bbch) (817)1RB2RA1LB_0LC0RA1LA_2LA0RB---
(bbch) (818, equivalent to 21 and 92)
The halting problems for Group 1 machines are highly dependent on the halting problem for machine 816. If it is non-halting, then 21, 92, 683, 817, and 818 are all non-halting. If 816 halts via transition C0, then 817 halts. If 816 halts via transition C2, then 21, 92, 683 and 818 all halt.
1RB2LA1LC_1LA2RB1RB_---2LB0LC
(bbch) (543). See argument for non-halting by @dyuan on 16 May 2025 and 5 January 2025.1RB1LC1LC_1LA2RB0RB_2LB---0LA
(bbch) (412) (cosearch). Longitudinal analysis by @Legion implies non-halting.1RB2LB0LC_2LA2RA1RB_---2LA1LC
(bbch) (650) (cosearch). Longitudinal analysis (with extra typo disclaimer) by @Legion implies non-halting.
1RB0RC---_2RC0LB1LB_2LC2RA2RB
(bbch) (279). Longitudinal analysis by @Legion implies non-halting.1RB2LA2RA_1LC1LB0RA_2RA0LB---
(bbch) (637). Analyzed by @Justin, proven by @dyuan and @Andrew.1RB2RB---_1LC2LB1RC_0RA0LB1RB
(bbch) (834, related to Group 1). See argument from @dyuan for similarity to 642.1RB2RB1LC_1LA2RB0RB_2LB---0LA
(bbch) (867). Longitudinal analysis by @Legion implies non-halting.
These TMs on the 9 Jun 2024 list have formal proofs.
1RB1LC---_0LC2RB1LB_2LA0RC1RC
(bbch) (400, equivalent to 494). Coq proof by @-d. Equivalence argument provided by @Legion.
1RB2LA0LA_2LC---2RA_0RA2RC1LC
(bbch) (494, equivalent to 400, non-halting certified on @lijil's list, equivalence not certified)1RB2LB---_1RC2RB1LC_0LA0RB1LB
(bbch) (642, related to Group 1) (cosearch). Coq proof by @-d. See argument for non-halting by @dyuan.