[Decider] Backward reasoning

Thank you very much for the details on your idea. I think it is very promising and, in my opinion, especially once we can plug this verification data into formal Lean/Coq proofs to get an absolute certificate of non-halting for the machine.

At the moment, we have put in place a Deciders’ validation process which requires that a decider decides at least 10% of the currently undecided machines which is why, under this “rule”, we would not officially apply the new 566 Translated Cyclers or other Translated Cyclers found in Skelet machines that are Translated Cyclers because its such a tiny fraction of the millions of machines that are left. Note that we have been consistent with this rule since the 5,647 machines of Closed state/transition cluster were not applied because it does not go above the 10% threshold.

The incentive behind this rule is to focus on new deciders, hopefully conceptually simple, that will slash the number of machines by a lot at once.

I believe that we could shift to your idea (i.e. immediately considering that a machine is decided given its verification data) once we get somewhere under 100k machines left.

Long story short: I think your idea is very certainly the way to go once we have reached a “small” set of undecided machines (in my mind, around 100,000).

The reason I expressed uncertainty about where to post all this was that it seems too general to post under [Decider] Backward Reasoning, but I couldn’t find a more suitable discussion branch for it.

I believe that you could post it here if it is about Backward Reasoning or in [Decider] Translated cyclers if it is about translated cyclers :slight_smile:

Thank you again!