User:RobinCodes/Work on BB Domains: Difference between revisions
RobinCodes (talk | contribs) (Rollback) Tag: Manual revert |
RobinCodes (talk | contribs) (Updated table.) |
||
| (6 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. | ||
As of | As of 29/09/2025 | ||
{| class="wikitable" | {| class="wikitable" | ||
|+ | |+ | ||
| Line 12: | Line 12: | ||
!7-state | !7-state | ||
!'''8-state''' | !'''8-state''' | ||
|- | |- | ||
!2-symbol | !2-symbol | ||
| Line 21: | Line 19: | ||
|0 Holdouts | |0 Holdouts | ||
July 2, 2024 | July 2, 2024 | ||
|1, | |1,686 Holdouts | ||
| | Exhausted (decider-wise) | ||
|22,721,168 Holdouts, Phase 2 Stage 4 in-progress | |||
|??? | |??? | ||
|- | |- | ||
!3-symbol | !3-symbol | ||
|0 Holdouts | |0 Holdouts | ||
|4+4 Holdouts BB3x3 month October | |4+4 Holdouts | ||
Exhausted (decider-wise) | |||
BB3x3 month October | |||
(4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | (4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | ||
1 Cryptid | 1 Cryptid | ||
| | |50,835,926 | ||
Terry Ligocki (6 passes done, error found, currently rerunning) | |||
Andrew Ducharme filtering with Ligockis' code (2 passes, more in-progress) | |||
|??? | |??? | ||
| | | | ||
| | | | ||
| Line 43: | Line 43: | ||
|0 Holdouts | |0 Holdouts | ||
Aug. 22, 2024 | Aug. 22, 2024 | ||
| | |64,777,377 | ||
[[User:XnoobSpeakable|XnoobSpeakable]] and Lúkos currently filtering | |||
(1 pass done) | |||
|??? | |??? | ||
| | | | ||
| | | | ||
| Line 58: | Line 59: | ||
2+4 Cryptids (4 probable) | 2+4 Cryptids (4 probable) | ||
|??? | |??? | ||
| | | | ||
| | | | ||
| Line 67: | Line 66: | ||
|- | |- | ||
!6-symbol | !6-symbol | ||
|873,469 Holdouts | |873,469-1 | ||
Holdouts | |||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
1 by hand | |||
|??? | |??? | ||
| | | | ||
| | | | ||
| Line 80: | Line 80: | ||
!7-symbol | !7-symbol | ||
|???? | |???? | ||
| | | | ||
| | | | ||
| Line 89: | Line 87: | ||
| | | | ||
|} | |} | ||
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. | |||
Latest revision as of 11:32, 4 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 29/09/2025
| Domain | 2-state | 3-state | 4-state | 5-state | 6-state | 7-state | 8-state |
|---|---|---|---|---|---|---|---|
| 2-symbol | 0 Holdouts | 0 Holdouts | 0 Holdouts | 0 Holdouts
July 2, 2024 |
1,686 Holdouts
Exhausted (decider-wise) |
22,721,168 Holdouts, Phase 2 Stage 4 in-progress | ??? |
| 3-symbol | 0 Holdouts | 4+4 Holdouts
Exhausted (decider-wise) BB3x3 month October (4 informal longitudinal proofs by @Legion) 1 Cryptid |
50,835,926
Terry Ligocki (6 passes done, error found, currently rerunning) Andrew Ducharme filtering with Ligockis' code (2 passes, more in-progress) |
??? | |||
| 4-symbol | 0 Holdouts
Aug. 22, 2024 |
64,777,377
XnoobSpeakable and Lúkos currently filtering (1 pass done) |
??? | ||||
| 5-symbol | 75 Holdouts
Exhausted (decider-wise) Some informal proofs exist 2+4 Cryptids (4 probable) |
??? | |||||
| 6-symbol | 873,469-1
Holdouts Exhausted (decider-wise) 1 by hand |
??? | |||||
| 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 completely (almost) unexplored.