A simple formalization and proof for the mutilated chess board

2001/05/01 by Lawrence C. Paulson · 2 citations
Computer Science · Mathematics · #Logic, programming, and type systems #Artificial Intelligence in Games #Formal Methods in Verification #Mathematical proof #Impossibility #Simple (philosophy) #Computer science #Abstraction #Object (grammar) #Calculus (dental) #Theoretical computer science #Programming language #Algebra over a field #Mathematics #Artificial intelligence #Pure mathematics #Epistemology #Philosophy #Geometry

paper · doi:10.1093/jigpal/9.3.475

openalex publication_date 2001/05/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30

Abstract

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.

Citations

• On sets, types, fixed points, and checkerboards
• An interactive solution to the n x n mutilated checkerboard problem
• Formal and Informal Proofs

Cited by

• A Problem with the Dependence of Informal Proofs on Formal Proofs
• Mutilated chessboard problem [wikipedia]