User:RobinCodes/Work on BB Domains: Difference between revisions
RobinCodes (talk | contribs) Updated page to be up-to-date with current results. |
RobinCodes (talk | contribs) Added BB3,4 results |
||
| (4 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. | 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 | As of 08/10/2025 | ||
Only domains with active filtering going on (decider-wise): BB(3,4) [Stage | 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 30: | Line 30: | ||
!3-symbol | !3-symbol | ||
|0 | |0 | ||
|4+ | |4+3 | ||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
( | (3 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | ||
1 Cryptid | 1 Cryptid | ||
| | | ~21.1M | ||
Terry Ligocki Phase 2, Stage | Terry Ligocki Phase 2, Stage 3 inprogress | ||
|?????????????? | |?????????????? | ||
| | | | ||
| Line 46: | Line 46: | ||
|0 | |0 | ||
Aug. 22, 2024 | Aug. 22, 2024 | ||
| | |17,983,810 | ||
[[User:XnoobSpeakable|XnoobSpeakable]] and [[User:WarpedWartWars|Lúkos]] currently filtering | [[User:XnoobSpeakable|XnoobSpeakable]] and [[User:WarpedWartWars|Lúkos]] currently filtering | ||
Phase 2, Stage | Phase 2, Stage 6 inprogress | ||
|????????????? | |????????????? | ||
| | | | ||
| Line 57: | Line 57: | ||
|- | |- | ||
!5-symbol | !5-symbol | ||
|75 | |75 | ||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
7 informal => 68 holdouts | |||
2+4 Cryptids (4 probable) | 2+4 Cryptids (4 probable) | ||
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.