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

From BusyBeaverWiki
Jump to navigation Jump to search
RobinCodes (talk | contribs)
Updated table.
RobinCodes (talk | contribs)
Added BB3,4 results
 
(7 intermediate revisions by 2 users 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.
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)


As of 29/09/2025
As of 08/10/2025
 
Only domains with active filtering going on (decider-wise): BB(3,4) [Stage 6] Xnoob and Lúkos, BB(4,3) [Stage 3] Terry Ligocki, BB(7) [Stage 4] Andrew Ducharme
{| class="wikitable"
{| class="wikitable"
|+
|+
Line 14: Line 16:
|-
|-
!2-symbol
!2-symbol
|0 Holdouts
|0
|0 Holdouts
|0
|0 Holdouts
|0
|0 Holdouts
|0
July 2, 2024
July 2, 2024
|1,686 Holdouts
|1,674
(2 informal)
Exhausted (decider-wise)
Exhausted (decider-wise)
|22,721,168 Holdouts, Phase 2 Stage 4 in-progress
|22,721,168 Phase 2, Stage 4
|???
inprogress
|?????
|-
|-
!3-symbol
!3-symbol
|0 Holdouts
|0
|4+4 Holdouts
|4+3
Exhausted (decider-wise)
Exhausted (decider-wise)
BB3x3 month October
 
(4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion)
(3 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion)
 
1 Cryptid
1 Cryptid
|50,835,926
| ~21.1M
Terry Ligocki (6 passes done, error found, currently rerunning)
Terry Ligocki Phase 2, Stage 3 inprogress
 
|??????????????
Andrew Ducharme filtering with Ligockis' code (2 passes, more in-progress)
|???
|
|
|
|
Line 41: Line 44:
|-
|-
!4-symbol
!4-symbol
|0 Holdouts
|0
Aug. 22, 2024
Aug. 22, 2024
|64,777,377
|17,983,810
[[User:XnoobSpeakable|XnoobSpeakable]] and Lúkos currently filtering
[[User:XnoobSpeakable|XnoobSpeakable]] and [[User:WarpedWartWars|Lúkos]] currently filtering


(1 pass done)
Phase 2, Stage 6 inprogress
|???
|?????????????
|
|
|
|
Line 54: Line 57:
|-
|-
!5-symbol
!5-symbol
|75 Holdouts
|75
Exhausted (decider-wise)
Exhausted (decider-wise)
Some informal proofs exist
7 informal => 68 holdouts
 
2+4 Cryptids (4 probable)
2+4 Cryptids (4 probable)
|???
|?????????????
|
|
|
|
Line 66: Line 70:
|-
|-
!6-symbol
!6-symbol
|873,469-1
|870,085
Holdouts
Exhausted (decider-wise)
Exhausted (decider-wise)
 
|?????????????
1 by hand
|???
|
|
|
|
Line 79: Line 80:
|-
|-
!7-symbol
!7-symbol
|????
|?????????
|
|
|
|
Line 87: 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 completely (almost) unexplored.
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 15:22, 14 October 2025

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)

As of 08/10/2025

Only domains with active filtering going on (decider-wise): BB(3,4) [Stage 6] Xnoob and Lúkos, BB(4,3) [Stage 3] Terry Ligocki, BB(7) [Stage 4] Andrew Ducharme

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,674

(2 informal) Exhausted (decider-wise)

22,721,168 Phase 2, Stage 4

inprogress

?????
3-symbol 0 4+3

Exhausted (decider-wise)

(3 informal longitudinal proofs by @Legion)

1 Cryptid

~21.1M

Terry Ligocki Phase 2, Stage 3 inprogress

??????????????
4-symbol 0

Aug. 22, 2024

17,983,810

XnoobSpeakable and Lúkos currently filtering

Phase 2, Stage 6 inprogress

?????????????
5-symbol 75

Exhausted (decider-wise) 7 informal => 68 holdouts

2+4 Cryptids (4 probable)

?????????????
6-symbol 870,085

Exhausted (decider-wise)

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