I’ve been building a library of Finite Automata Reduction proofs for 5-state TMs: in this repo with complete automta and some more info, and in the original shorter Decider Verification File format on Dropbox (index/DVF).
A remarkable finding has been that nearly all infinite 5-state TMs have proofs in this format. In fact, this proof library covers the entire undecided index with just 34 exceptions. (I plan to expand it to cover all previously decided machines too. The bbchallenge community is still working on a way to find all of these proofs from scratch, quickly, using accepted deciders.)
4 of these are bouncers of the form decided by Tony’s decider – thus they’re known to be provable by CTL, and there’s just some computation needed to find acceptably small proofs. It’s possible some of these will hit limitations of the binary DVF format. They are these three things and Skelet 20.
Those aren’t so interesting, but for the rest, I’ve compiled a holdout-zoology.zip file (945.9 KB) classifying them, with seed IDs and diagrams and links to analyses. There’s also a catalog showing my classification maps onto Skelet’s.
(The two "pointy-wide’ machines in this zip file are now historical. I wrote more about them here.)
The rest are holdouts for Skelet’s program and all of the community’s deciders to date. Most have proofs or strong heuristic arguments that CTL solutions (specifically, finding a regular language separating the set of reachable configurations from the set of halting configurations) are impossible
Skelet 1 is believed to be a translated cycler, thus theoretically CTLable, but with a preposterously long period and little hope of having a solution in this proof format.
Skelet 10 is manually proven by Dan Briggs and with a neat interpretation by Shawn Ligocki. There’s a heuristic argument that finite-state classifiers are insufficient – to analyze a configuration requires some counting.
5 more Skelet machines are classified as shift-overflow counters by Shawn, and believed to be proven. There’s similarly a heuristic argument about these.
Skelet 17 is being analyzed on Discord – it looks like the case is nearly cracked.
The “counter-balanced” class maps onto a subset of what Skelet calls “Shift Recursive” machines. Konrad Deka has analyzed one on Discord, giving a quick proof that it’s infinite and a strong heuristic argument that it’s not CTLable (also due to a need to count).
The “counter-inverted” class also maps into Skelet’s “Shift Recursive” class. Skelet wrote a non-halting argument for one.
The “cubic-finned” class effectively operates on a pair of unary numbers. @Iijil analyzed one and provided the first known proof that a naturally occurring TM has reachable and halting configuration sets which no regular language can separate.
The “cubic-helix” class is expected to have a similar obstacle (and easy proof of infinitude), though this hasn’t been done yet.
If interested, check out the zip file. In addition, here are the machine strings:
1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE
1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA
1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC
1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA
1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB
1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE
1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD
1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE
1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE
1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE
1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE
1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE
1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC
1RB0RE_1RC1RE_1LD---_1LA1LE_1RA0LD
1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE
1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE
1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA
1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA
1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE
1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC
1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC
1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---
1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA
1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE
1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA
1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB
1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD
1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC
1RB1RD_1LC0LD_1LE1LD_1LB0RA_1RA---
1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC
1RB1RD_1LC---_1LE1LD_1RE0LC_1RA0RD
1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA
1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA
1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA