User:RobinCodes/Work on BB Domains: Difference between revisions
RobinCodes (talk | contribs) Updated table. |
RobinCodes (talk | contribs) Updated values. Updated table formatting. Added "active filtering domains". |
||
| 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. | ||
As of | As of 08/10/2025 | ||
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" | ||
|+ | |+ | ||
| Line 14: | Line 16: | ||
|- | |- | ||
!2-symbol | !2-symbol | ||
|0 | |0 | ||
|0 | |0 | ||
|0 | |0 | ||
|0 | |0 | ||
July 2, 2024 | July 2, 2024 | ||
|1, | |1,674 | ||
(2 informal) | |||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
|22,721,168 | |22,721,168 Phase 2, Stage 4 | ||
|??? | inprogress | ||
|????? | |||
|- | |- | ||
!3-symbol | !3-symbol | ||
|0 | |0 | ||
|4+4 Holdouts | |4+4 Holdouts | ||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
(4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | (4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | ||
1 Cryptid | 1 Cryptid | ||
| | |~33.8M Holdouts | ||
Terry Ligocki | Terry Ligocki Phase 2, Stage 2 inprogress | ||
|?????????????? | |||
|??? | |||
| | | | ||
| | | | ||
| Line 41: | Line 44: | ||
|- | |- | ||
!4-symbol | !4-symbol | ||
|0 | |0 | ||
Aug. 22, 2024 | Aug. 22, 2024 | ||
| | |37,016,957 | ||
[[User:XnoobSpeakable|XnoobSpeakable]] and Lúkos currently filtering | [[User:XnoobSpeakable|XnoobSpeakable]] and Lúkos currently filtering | ||
Phase 2, Stage 3 inprogress | |||
|??? | |????????????? | ||
| | | | ||
| | | | ||
| Line 56: | Line 59: | ||
|75 Holdouts | |75 Holdouts | ||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
Some informal proofs exist | Some informal proofs exist | ||
2+4 Cryptids (4 probable) | 2+4 Cryptids (4 probable) | ||
|??? | |????????????? | ||
| | | | ||
| | | | ||
| Line 66: | Line 71: | ||
|- | |- | ||
!6-symbol | !6-symbol | ||
| | |870,085 | ||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
|????????????? | |||
|??? | |||
| | | | ||
| | | | ||
| Line 79: | Line 81: | ||
|- | |- | ||
!7-symbol | !7-symbol | ||
|???? | |????????? | ||
| | | | ||
| | | | ||
| Line 87: | Line 89: | ||
| | | | ||
|} | |} | ||
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 | 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. | ||
Revision as of 16:23, 8 October 2025
Page to collect the BB Domains and their status. Holdout counts are machines that do not have a formal Rocq proof.
As of 08/10/2025
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
| 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+4 Holdouts
Exhausted (decider-wise) (4 informal longitudinal proofs by @Legion) 1 Cryptid |
~33.8M Holdouts
Terry Ligocki Phase 2, Stage 2 inprogress |
?????????????? | |||
| 4-symbol | 0
Aug. 22, 2024 |
37,016,957
XnoobSpeakable and Lúkos currently filtering Phase 2, Stage 3 inprogress |
????????????? | ||||
| 5-symbol | 75 Holdouts
Exhausted (decider-wise) Some informal proofs exist 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.