Almost in sync with April 7th, International Beaver Day, after a long validation process, we are today officially applying the results of [Decider] Finite Automata Reduction (formally described here), initially introduced by Justin Blanchard @UncombedCoconut.
In a nutshell, Finite Automata Reduction (FAR) searches for a regular language that contains all of a TM’s eventually-halting configurations (with finitely many 1s). That way, if the initial blank configuration is not part of the regular language, we know that the machine does not halt from it. This technique relates closely to historical CTL methods that have been developed in the field (credited to @heiner in collaboration with J. Buntrock), however, its main originality is that, instead of looking for regular expressions, it constructs a Nondeterministic Finite Automaton based on an original (and clever!) optimization algorithm over matrices.
If you are in for all of the details, the method is presented formally at length in this document (Section 6).
Official 32,632 holdouts. The method is efficient as it decided 503,169 machines out of 535,801 (94%), in a bit less than 30 minutes on a regular laptop. We are left with 32,632 machines to decide! Find these 32,632 machines on our undecided index repository.
Justin’s 38 holdouts. A great property of Finite Automata Reduction is that it is very well suited for verification. This means that FAR, for a TM that it decides, can provide a certificate (essentially consisting of a Nondeterministic Finite Automaton) of nonhalting that is easy to verify – see Theorem 20 and Remark 21. By pushing the parameters of FAR to month-long computations and by using techniques that are not fully documented (yet), Justin Blanchard (@UncombedCoconut ) has been able to provide FAR certificates for another 32,594 machines, leaving only 38 machines with 5 states undecided: Justin’s 38 holdouts. Although these extra 32,594 certificates are believed to be valid (they were checked by 3 independent implementations), we do not include them in today’s release because they are currently hard to reproduce.
Other news: Skelet 1 is probably infinite. An historically hard machine to decide is Skelet’s machine #1 (note that it is also in Justin’s 38 holdouts!) – see our page on Skelet’s machine. Recently, Shawn Ligocki (@sligocki ) and Pavel Kropitz (@univerz ), thanks to accelerated simulations, have reached the conclusion that Skelet 1 is a Translated Cycler – i.e. it eventually repeats a spatially translated pattern. Numbers are staggering, it would start repeating way after 10^24 steps and the period would be 8,468,569,863 steps long. This result has not been independently verified yet, do you want to try? More on this on Shawn’s blog.
Acknowledgement. This spring release would have not been possible without the dedicated work and extreme patience of Justin Blanchard (@UncombedCoconut ) who originally came up with FAR and then went through our validation process. Many thanks to Justin for this big beavering leap! Others have contributed to this method by producing alternative implementations or discussing and writing the formal proof presented here: Tony Guilfoyle, Tristan Stérin (cosmo), Nathan Fenner, Mateusz Naściszewski (Mateon1), Konrad Deka, Iijil, Shawn Ligocki.
So, happy International Beaver Day to all and let’s continue busy beavering our way through the last remaining 32,632 machines! 
