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

From BusyBeaverWiki
Jump to navigation Jump to search
RobinCodes (talk | contribs)
Update Phase 2 Stage 6 completed (BB(3x4))
RobinCodes (talk | contribs)
Added "informal/unverified proofs" section. Improved overall flow and structure of the page.
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. (Grouped by machine behaviour)
== Progress by domain ==
As of 25 October 2025:


As of 08/10/2025
<code>Only domains with active filtering going on (decider-wise): BB(7) Terry Ligocki</code>
 
Only domains with active filtering going on (decider-wise): BB(7) Terry Ligocki  
{| class="wikitable"
{| class="wikitable"
|+
|+
Line 23: Line 22:
|1,616
|1,616
(2 informal)
(2 informal)
Exhausted (decider-wise)
Exhausted


15 Cryptids found
15 Cryptids found
|22,721,168 Phase 2, Stage 4  
|22,721,168 Phase 2, Stage 4  
|?????
|???
|-
|-
!3-symbol
!3-symbol
|0
|0
|4+3
|4+3
Exhausted (decider-wise)
Exhausted


(3 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion)
(3 informal)


1 Cryptid
1 Cryptid
| 9,401,447  
| 9,401,447  
Terry Ligocki Phase 2, Stage 2
Terry Ligocki Phase 2, Stage 2
|??????????????
|???
|
|
|
|
Line 51: Line 50:


Phase 2, Stage 6
Phase 2, Stage 6
|?????????????
|???
|
|
|
|
Line 59: Line 58:
!5-symbol
!5-symbol
|75
|75
Exhausted (decider-wise)
Exhausted
8 informal => 67 holdouts
(8 informal)


2+4 Cryptids (4 probable)
2+4 Cryptids (4 probable)
|?????????????
|???
|
|
|
|
Line 72: Line 71:
!6-symbol
!6-symbol
|870,085
|870,085
Exhausted (decider-wise)
Exhausted
|?????????????
|???
|
|
|
|
Line 81: Line 80:
|-
|-
!7-symbol
!7-symbol
|?????????
|???
|
|
|
|
Line 89: Line 88:
|
|
|}
|}
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.
<small>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.</small>
 
== Informal and unverified proofs by domain ==
'''Unconfirmed, informal proofs of machines for each domain by equivalence class:'''
{| class="wikitable"
!Domain
!2-state
!3-state
!4-state
!5-state
!6-state
|-
!2-symbol
|0
|0
|0
|0
|3
|-
!3-symbol
|0
|1
| ----
| ---
| ---
|-
!4-symbol
|0
| ---
| ---
| ---
| ---
|-
!5-symbol
|7
| ---
| ---
| ---
| ---
|}
 
=== [[BB(6)]]: 25 October 2025 ===
 
===== 3 informal, 1 unconfirmed (2 informal 1 unconfirmed by eqv. class) =====
 
* [https://discord.com/channels/960643023006490684/1239205785913790465/1431135577234997299 Bricks / Shawn Ligocki:] 1RB1RF_0LC1RC_1RD1LC_---0RE_1RA1LF_1RA0LE NONHALT (verified by quick_sim.py)
* [https://discord.com/channels/960643023006490684/1239205785913790465/1431225455557611611 Racheline]:
*# >1RB0RB_1LB0LC_1RD1LC_1RE0RA_1RF0RB_---1LB
*# 1RB0RB_1LB0LC_1RD1LC_1RE0RA_0RF0RB_---0LA (equivalence)
* [https://discord.com/channels/960643023006490684/1421782442213376000/1431483206208852001 Shawn, star, Pomme, @mxdys]: BMO 7, unconfirmed
 
=== [[BB(3,3)]]: 25 October 2025 ===
 
===== 3 informal, 1 unconfirmed by eqv. class and individual =====
 
* 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 ===
 
===== 8 informal, (7 by eqv. class) =====
 
* Dyuan:
*# [[Beaver Math Olympiad#3. 1RB0RB3LA4LA2RA 2LB3RA---3RA4RB (bbch) and 1RB1RB3LA4LA2RA 2LB3RA---3RA4RB (bbch)|BMO 3]] (2 machines) ([https://discord.com/channels/960643023006490684/1084047886494470185/1252634913220591728 source])
*# 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA ([https://discord.com/channels/960643023006490684/1259770421046411285/1290449717536489622 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])
*# 1RB3LA4LA2RB1LA_2LA4RB---3RA3LA ([https://discord.com/channels/960643023006490684/1084047886494470185/1254518334406266964 3])
* [https://discord.com/channels/960643023006490684/1259770421046411285/1329663999700111471 Racheline]: 1RB2LB---4LB0RB_1LA3RB4RB4RA1LB
* [https://discord.com/channels/960643023006490684/1259770421046411285/1428501877947109437 Peacemaker II]: 1RB2LA0LB1LA2RA_0LA3RA1RA4LB---

Revision as of 13:37, 25 October 2025

Progress by domain

As of 25 October 2025:

Only domains with active filtering going on (decider-wise): BB(7) Terry Ligocki

Domain 2-state 3-state 4-state 5-state 6-state 7-state 8-state
2-symbol 0 0 0 0

July 2, 2024

1,616

(2 informal) Exhausted

15 Cryptids found

22,721,168 Phase 2, Stage 4 ???
3-symbol 0 4+3

Exhausted

(3 informal)

1 Cryptid

9,401,447

Terry Ligocki Phase 2, Stage 2

???
4-symbol 0

Aug. 22, 2024

15,564,491

XnoobSpeakable and Lúkos currently filtering

Phase 2, Stage 6

???
5-symbol 75

Exhausted (8 informal)

2+4 Cryptids (4 probable)

???
6-symbol 870,085

Exhausted

???
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.

Informal and unverified proofs by domain

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

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

BB(6): 25 October 2025

3 informal, 1 unconfirmed (2 informal 1 unconfirmed by eqv. class)

BB(3,3): 25 October 2025

3 informal, 1 unconfirmed by eqv. class and individual
  • 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

8 informal, (7 by eqv. class)
  • Dyuan:
    1. BMO 3 (2 machines) (source)
    2. 1RB4LA1LB2LA0RB_2LB3RB4LA---1RA (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---