# Knight's Tour Revisited Revisited

 Title: Knight's Tour Revisited Revisited Author: Lukas Koller (lukas /dot/ koller /at/ tum /dot/ de) Submission date: 2022-01-04 Abstract: This is a formalization of the article Knight's Tour Revisited by Cull and De Curtins where they prove the existence of a Knight's path for arbitrary n × m-boards with min(n,m) ≥ 5. If n · m is even, then there exists a Knight's circuit. A Knight's Path is a sequence of moves of a Knight on a chessboard s.t. the Knight visits every square of a chessboard exactly once. Finding a Knight's path is a an instance of the Hamiltonian path problem. A Knight's circuit is a Knight's path, where additionally the Knight can move from the last square to the first square of the path, forming a loop. During the formalization two mistakes in the original proof were discovered. These mistakes are corrected in this formalization. BibTeX: @article{Knights_Tour-AFP, author = {Lukas Koller}, title = {Knight's Tour Revisited Revisited}, journal = {Archive of Formal Proofs}, month = jan, year = 2022, note = {\url{https://isa-afp.org/entries/Knights_Tour.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License