User:RobinCodes/Work on BB Domains: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
Lúkos user page link; hope you're fine with me editing your page
RobinCodes (talk | contribs)
Progress by domain: Changed date
 
(50 intermediate revisions by the same user not shown)
Line 1: Line 1:
Page to collect the BB Domains and their status. Holdout counts are machines that do not have a formal Rocq proof.
== Progress by domain ==
As of 19 December 2025:


As of 08/10/2025
<code>Only domains with active filtering going on (decider-wise): BB(3,4) - XnoobSpeakable and Lúkos</code> 


Only domains with active filtering going on (decider-wise): BB(3,4) [Stage 3] Xnoob and Lúkos, BB(4,3) [Stage 2] Terry Ligocki, BB(7) [Stage 4] Andrew Ducharme
{| class="wikitable"
{| class="wikitable"
|+
|+ Work on BB Domains
! !!2-state!!3-state !!4-state!!5-state!!6-state
!7-state
|- 
! 2-symbol
| [[BB(2)]] = 6
| [[BB(3)]] = 21
| [[BB(4)]] = 107
| [[BB(5)]] = 47,176,870
2 Jul 2024
| style="background: orange;" | 1342
[https://docs.google.com/spreadsheets/d/1mMp8bAcTFT91j7azn72liX8NSTwc2E_ozKnOGTfRCfw/edit?gid=1330361301#gid=1330361301 Holdouts list]
16+8 Cryptids, Exhausted
| style="background: orange;" | 20,405,295
No Handwork
Andrew Ducharme,
Terry Ligocki
Phase 2, Stage 5
|-
! 3-symbol
| [[BB(2,3)]] = 38
| style="background: orange;" | 4
[[BB(3,3)#Holdouts|Holdouts list]]
(3 informal)
1 Cryptid, Exhausted
| style="background: #ffe4b2;" | 9,401,447
No Handwork
Terry Ligocki Phase 2, Stage 2
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|-
! 4-symbol 
| [[BB(2,4)]] = 3,932,964
| style="background: #ffe4b2;" | 14,413,460
No Handwork
[[User:XnoobSpeakable|XnoobSpeakable,]] [[User:WarpedWartWars|Lúkos]]
 
Phase 2, Stage 10 in-progress
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|-
! 5-symbol
| style="background: orange;" | 64
[[BB(2,5)#Holdouts|Holdouts list]]
(11 informal)
 
2+4 Cryptids
| style="background: #ffe4b2;" |[[BB(3,5)]]
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|-
! 6-symbol
| style="background: #ffe4b2;" | 870,085
No Handwork, Exhausted
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|-
!7-symbol
| style="background: #ffe4b2;" |Enumeration started!
06xxx done
 
(7/100)
 
Expected no. of holdouts: 3B
 
Current: 210M
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
| style="background: #ffe4b2;" |
|}
 
== Enumeration ==
The enumeration process for [[BB(2,7)]] has started, and 5% has so far been completed. [[BB(8)]] is (tested from a random sample) even harder to enumerate. These processes will take a very long time and much collaborative work to complete. As for BB(3x5), BB(4x4), BB(5x3), enumeration may still be possible, but also incredibly difficult. Any domains after these are probably complete out-of-reach of current technology.
 
== Informal and unverified proofs by domain ==
'''Unconfirmed, informal proofs of machines for each domain by equivalence class: 13 total'''
{| class="wikitable"
!Domain
!Domain
!2-state
!2-state
Line 12: Line 98:
!5-state
!5-state
!6-state
!6-state
!7-state
!'''8-state'''
|-
|-
!2-symbol
!2-symbol
Line 20: Line 104:
|0
|0
|0
|0
July 2, 2024
|'''1'''
|1,674
(2 informal)
Exhausted (decider-wise)
|22,721,168 Phase 2, Stage 4
inprogress
|?????
|-
|-
!3-symbol
!3-symbol
|0
|0
|4+4 Holdouts
|'''3'''
Exhausted (decider-wise)
| ----
 
| ---
(4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion)
| ---
 
1 Cryptid
|~33.8M Holdouts
Terry Ligocki Phase 2, Stage 2 inprogress
|??????????????
|
|
|
|-
|-
!4-symbol
!4-symbol
|0
|0
Aug. 22, 2024
| ---
|37,016,957
| ---
[[User:XnoobSpeakable|XnoobSpeakable]] and [[User:WarpedWartWars|Lúkos]] currently filtering
| ---
 
| ---
Phase 2, Stage 3 inprogress
|?????????????
|
|
|
|
|-
|-
!5-symbol
!5-symbol
|75 Holdouts
|'''9'''
Exhausted (decider-wise)
| ---
| ---
| ---
| ---
|}
<small>'''13''' total by eqv. class and proof count. 15 by individual machine.</small>
 
=== [[BB(6)]]: 16 December 2025 ===
 
===== 1 informal =====
 
* Likely correct: (1)
** <s>[https://discord.com/channels/960643023006490684/1421782442213376000/1431483206208852001 Shawn, star, Pomme, @mxdys]: BMO 7 verified</s>
** mxdys, Pomme, Autumn Pan, vyx<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1441124403801755730 <nowiki>[1]</nowiki>][https://discord.com/channels/960643023006490684/1443295684878143579/1443295684878143579 <nowiki>[2]</nowiki>][https://discord.com/channels/960643023006490684/1443295684878143579/1444047803935490190 <nowiki>[3]</nowiki>][https://discord.com/channels/960643023006490684/1443295684878143579/1444051070186819836 <nowiki>[4]</nowiki>]</sup>: <code>1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---</code>
 
=== [[BB(3,3)]]: 25 October 2025 ===
 
===== 3 informal =====
 
* Legion: ([[Longitudinal Analysis|long. analysis]]) informal
*# 1RB2LB0LC_2LA2RA1RB_---2LA1LC ([https://discord.com/channels/960643023006490684/1259770474897080380/1290044219481657476 <small>1</small>])
*# 1RB1LC1LC_1LA2RB0RB_2LB---0LA ([https://discord.com/channels/960643023006490684/1259770474897080380/1279055891559223399 2])
*# 1RB0RC---_2RC0LB1LB_2LC2RA2RB ([https://discord.com/channels/960643023006490684/1084047886494470185/1256729514076016733 3])
 
* [https://discord.com/channels/960643023006490684/1259770474897080380/1430531925315031172 @furnleaf]: 1RB1LB2LC_1LA2RB1RB_---0LA2LA (397) ''erroneous'', [https://discord.com/channels/960643023006490684/1259770474897080380/1430557898269790248 currently attempting fix]
 
=== [[BB(2,5)]]: 25 October 2025 ===


Some informal proofs exist
===== 9 informal, 2 unverified (8 informal, 1 unverified by eqv. class) =====


2+4 Cryptids (4 probable)
* Dyuan:
|?????????????
*# [[Beaver Math Olympiad#3. 1RB0RB3LA4LA2RA 2LB3RA---3RA4RB (bbch) and 1RB1RB3LA4LA2RA 2LB3RA---3RA4RB (bbch)|BMO 3]] (2 machines in 1 eqv. class) ([https://discord.com/channels/960643023006490684/1084047886494470185/1252634913220591728 source])
|
*# 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA ([https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 source])
|
*# Dekaheptoid, unverified: [[1RB3RB1LB---2RB_2LA1RA4LB2LA2RA]] ([https://discord.com/channels/960643023006490684/1259770421046411285/1267650177389432913 source]), equivalently 1RB3RA2LB1LB1RB_2LA2RA4LA1LA---
|
*# BMO 3 variant: 1RB0RA3LA4LA2RA_2LB3LA---4RA3RB ([https://discord.com/channels/960643023006490684/1259770421046411285/1415337575543214132 source])
|
* Legion:
|
*# 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (<small>[https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 1]</small>)
|-
*# 1RB3LA4LA1LA2RA_2LA4RB---0RA0LA ([https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 2])
!6-symbol
*# 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA ([https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 3])
|870,085
* [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Racheline]: 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB
Exhausted (decider-wise)
* [https://discord.com/channels/960643023006490684/1259770421046411285/1428501877947109437 Peacemaker II]: 1RB2LA0LB1LA2RA_0LA3RA1RA4LB---
|?????????????
|
|
|
|
|
|-
!7-symbol
|?????????
|
|
|
|
|
|
|}
I also wanted to study at what point are domains infeasible with reasonable resources and time, but this is for the future of this page. ???? And after are almost completely unexplored.

Latest revision as of 18:29, 19 December 2025

Progress by domain

As of 19 December 2025:

Only domains with active filtering going on (decider-wise): BB(3,4) - XnoobSpeakable and Lúkos

Work on BB Domains
2-state 3-state 4-state 5-state 6-state 7-state
2-symbol BB(2) = 6 BB(3) = 21 BB(4) = 107 BB(5) = 47,176,870

2 Jul 2024

1342

Holdouts list 16+8 Cryptids, Exhausted

20,405,295

No Handwork Andrew Ducharme, Terry Ligocki Phase 2, Stage 5

3-symbol BB(2,3) = 38 4

Holdouts list (3 informal) 1 Cryptid, Exhausted

9,401,447

No Handwork Terry Ligocki Phase 2, Stage 2

4-symbol BB(2,4) = 3,932,964 14,413,460

No Handwork XnoobSpeakable, Lúkos

Phase 2, Stage 10 in-progress

5-symbol 64

Holdouts list (11 informal)

2+4 Cryptids

BB(3,5)
6-symbol 870,085

No Handwork, Exhausted

7-symbol Enumeration started!

06xxx done

(7/100)

Expected no. of holdouts: 3B

Current: 210M

Enumeration

The enumeration process for BB(2,7) has started, and 5% has so far been completed. BB(8) is (tested from a random sample) even harder to enumerate. These processes will take a very long time and much collaborative work to complete. As for BB(3x5), BB(4x4), BB(5x3), enumeration may still be possible, but also incredibly difficult. Any domains after these are probably complete out-of-reach of current technology.

Informal and unverified proofs by domain

Unconfirmed, informal proofs of machines for each domain by equivalence class: 13 total

Domain 2-state 3-state 4-state 5-state 6-state
2-symbol 0 0 0 0 1
3-symbol 0 3 ---- --- ---
4-symbol 0 --- --- --- ---
5-symbol 9 --- --- --- ---

13 total by eqv. class and proof count. 15 by individual machine.

BB(6): 16 December 2025

1 informal

BB(3,3): 25 October 2025

3 informal
  • Legion: (long. analysis) informal
    1. 1RB2LB0LC_2LA2RA1RB_---2LA1LC (1)
    2. 1RB1LC1LC_1LA2RB0RB_2LB---0LA (2)
    3. 1RB0RC---_2RC0LB1LB_2LC2RA2RB (3)

BB(2,5): 25 October 2025

9 informal, 2 unverified (8 informal, 1 unverified by eqv. class)
  • Dyuan:
    1. BMO 3 (2 machines in 1 eqv. class) (source)
    2. 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA (source)
    3. Dekaheptoid, unverified: 1RB3RB1LB---2RB_2LA1RA4LB2LA2RA (source), equivalently 1RB3RA2LB1LB1RB_2LA2RA4LA1LA---
    4. BMO 3 variant: 1RB0RA3LA4LA2RA_2LB3LA---4RA3RB (source)
  • Legion:
    1. 1RB2RA3LA4LA2RB_2LA---1LA1RA3RA (1)
    2. 1RB3LA4LA1LA2RA_2LA4RB---0RA0LA (2)
    3. 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA (3)
  • Racheline: 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB
  • Peacemaker II: 1RB2LA0LB1LA2RA_0LA3RA1RA4LB---