BB(3,3)

The 3-state, 3-symbol Busy Beaver problem, BB(3,3), is unsolved. With the discovery of the Cryptid machine Bigfoot in October 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 November 2007, proving the lower bounds:

$${\begin{array}{lcrl}S(3,3)&\geq &119{,}112{,}334{,}170{,}342{,}541&>10^{17}\\\Sigma (3,3)&\geq &374{,}676{,}383&>10^{8}\\\end{array}}$$

One of the 6 currently unsolved TMs, 1RB2LC1RC_2LC---2RB_2LA0LB0RA (bbch), is under exploration on Discord and believed to probviously halt. If it halts, it will be the new champion.

Cryptids

Known Cryptids:

• 1RB2RA1LC_2LC1RB2RB_---2LA1LA (bbch), known as Bigfoot

Potential Cryptids:

• 1RB2LC1RC_2LC---2RB_2LA0LB0RA (bbch)

Top Halters

The current top 10 BB(3,3) halters (known by Shawn Ligocki) are:

Standard format               Status S                  Σ
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, @tjligocki 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. These results were updated on 20 Mar 2025 in the same location and 76 machines remained on the 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. Together, this leaves 21 unsolved TMs, all of which were on @Justin Blanchard's informal holdouts list of 22 machines. The extra machine on Justin's list 1RB2LA0LA_2LC---2RA_0RA2RC1LC (bbch) had been solved by @lijil before, but this was not realized for some time.

On 26 Feb 2025, @mxdys published a list of 19 holdouts that withstood state-of-the-art Rocq deciders. Some of these machines already had fairly rigorous or even full Rocq proofs for non-halting, which were integrated into a 12 TM Rocq holdout list published on 24 Aug 2025.

Holdouts

This section is based on @mxdys's August 2025 holdouts list of 12 TMs.

Cryptids

• 1RB2RA1LC_2LC1RB2RB_---2LA1LA (bbch) (829), Bigfoot

Unsolved

• 1RB1LB2LC_1LA2RB1RB_---0LA2LA (bbch) (397)
• 1RB0LB0RC_2LC2LA1RA_1RA1LC--- (bbch) (153, equivalent to 758)
• 1RB2LC1RC_2LC---2RB_2LA0LB0RA (bbch) (758, equivalent to 153)
• 1RB2LA1LA_2LA0RA2RC_---0LC2RA (bbch) (531, equivalent to 532), Wily Coyote
• 1RB2LA1LA_2LA0RA2RC_---1RB2RA (bbch) (532, equivalent to 531)

Solved with moderate rigor

• 1RB2LA1LC_1LA2RB1RB_---2LB0LC (bbch) (543). See argument for non-halting by @dyuan on 16 May 2024 and 5 January 2025
• 1RB2LB0LC_2LA2RA1RB_---2LA1LC (bbch) (650) (cosearch). Longitudinal analysis (with extra typo disclaimer) by @Legion implies non-halting
• 1RB1LC1LC_1LA2RB0RB_2LB---0LA (bbch) (412) (cosearch). Longitudinal analysis by @Legion implies non-halting
• 1RB2RB1LC_1LA2RB0RB_2LB---0LA (bbch) (867). Longitudinal analysis by @Legion implies non-halting
• 1RB0RC---_2RC0LB1LB_2LC2RA2RB (bbch) (279). Longitudinal analysis by @Legion implies non-halting
• 1RB2LA1LA_0LA0RC0LC_---2RA1RA (bbch) (522) has FAR certificate

FAR(direction=R, transitions=[(0, 1, 2), (3, 4, 0), (5, 6, 7), (7, 0, 7), (7, 7, 7), (7, 7, 0), (8, 2, 1), (7, 7, 7), (7, 9, 10), (7, 11, 7), (7, 7, 7), (7, 7, 7)])

Interesting Rocq-Solved TMs

The following TMs have halting problems highly dependent on that of machine 816. While all TMs were solved individually, it was theoretically possible that someone solved machine 816 and solved up to four machines "for free." If 816 was non-halting, then 21, 92, 683, 817, and 818 were all non-halting. If 816 halted via transition C0, then 817 halted. And if 816 halted via transition C2, then 21, 92, 683 and 818 all halted. A compilation of the various analyses can be found here

• 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)

These TMs were on Justin Blanchard's informal holdouts list of 22 TMs but were Rocq-decided individually by @mxdys in their February 2025 release. Two other members of Justin Blanchard's list Rocq-decided by mxdys in February 2025 were 1RB2LB---_1RC2RB1LC_0LA0RB1LB (bbch) (642) and 1RB2RB---_1LC2LB1RC_0RA0LB1RB (bbch) (834). @-d independently generated a Rocq proof for 642 (cosearch), and @dyuan01 independently discovered non-halting arguments for 642 and 834, and noted their similarity.

Similarly, @-d independently wrote a Rocq proof for 1RB2LA0LA_2LC---2RA_0RA2RC1LC (bbch) (494) which was adapted into mxdys's pipeline in August of 2025. This release also adapted the proof to formally prove 1RB1LC---_0LC2RB1LB_2LA0RC1RC (bbch) (400), which was known to be equivalent to 494.

The August release also confirmed the non-halting status of 1RB2LA1RA_1LC1RC2RB_---1RA1LC (bbch) (575), 1RB2LA1RA_1LC2RC2RB_---1RA1LC (bbch) (585), and 1RB2LA1RA_2LC2RC2RB_---2LA1LC (bbch) (588), which, as first shown by @dyuan01 and @Justin Blanchard, infinitely enumerate the series $p_{n}=a2^{n}-(-1)^{n}b-\lfloor n/2\rfloor -c$ for machine-dependent constants a, b, and c.