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 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.
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