A simple formalization and proof for the mutilated chess board
Lawrence Charles Paulson · Logic Journal of IGPL · 2001
The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are straightforward except for some lemmas concerning finite cardinalities. This exercise is an object lesson in choosing a good formalization: one at the right level of abstraction.