As far as I am aware, all of the proofs and techniques for each machine were present before mxdys managed to get the whole theorem into Coq: the main problem wa

As far as I am aware, all of the proofs and techniques for each machine were present before mxdys managed to get the whole theorem into Coq: the main problem was that the deciders and manual proofs were disorganized and somewhat suspect. The worst offenders here were Skelet #1, which needed a bespoke program to accelerate it to its ultimate pattern [0], and Skelet #17, which took Xu seven pages' worth of dense reasoning to prove non-halting [1]. The full Coq proof put a much-needed degree of confidence into these results. [0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html https://www.sligocki.com/2023/03/13/skelet-1-infinite.html [1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/184 https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...