skelet17.pdf (202.6 KB)
Here is the latest draft of my paper. Although slight tweaks could be made, I’m confident that this version is fully rigorous.
You can find the machine here.
2 Likes
This proof has been formalized into Coq by @mxdys Coq-BB5/Skelet17.v at main · ccz181078/Coq-BB5 · GitHub with Human description Coq-BB5/Skelet17.md at main · ccz181078/Coq-BB5 · GitHub
1 Like
Here is an updated version of my proof, added references: http://chrisxudoesmath.com/papers/skelet17.pdf
1 Like