User:RobinCodes/Work on BB Domains: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) m (Fixed info) |
RobinCodes (talk | contribs) (Updated table.) |
||
| 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 21: | Line 21: | ||
|1,691 Holdouts | |1,691 Holdouts | ||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
| | |22,801,601 Holdouts, Phase 2 Stage 4 in-progress | ||
|??? | |??? | ||
|- | |- | ||
| Line 31: | Line 31: | ||
(4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | (4 informal [[Longitudinal Analysis|longitudinal]] proofs by @Legion) | ||
1 Cryptid | 1 Cryptid | ||
| | |84,066,821 | ||
Terry Ligocki (6 passes done) | Terry Ligocki (6 passes done) | ||
Andrew Ducharme filtering with Ligockis' code | |||
|??? | |??? | ||
| | | | ||
| Line 62: | Line 64: | ||
|- | |- | ||
!6-symbol | !6-symbol | ||
|873,469 Holdouts | |873,469-1 | ||
Holdouts | |||
Exhausted (decider-wise) | Exhausted (decider-wise) | ||
1 by hand | |||
|??? | |??? | ||
| | | | ||
| Line 80: | Line 85: | ||
| | | | ||
|} | |} | ||
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 19:23, 29 September 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,691 Holdouts
Exhausted (decider-wise) |
22,801,601 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 |
84,066,821
Terry Ligocki (6 passes done) Andrew Ducharme filtering with Ligockis' code |
??? | |||
| 4-symbol | 0 Holdouts
Aug. 22, 2024 |
434,787,751
XnoobSpeakable and Lúkos currently filtering |
??? | ||||
| 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.