### Abstract

This is a formalization of the article

BSD License*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.