The Mutilated Checkerboard Problem in the Lightweight Set Theory of Mizar
Piotr Rudnicki · 1996
An 8×8 checkerboard with two diagonally opposite squares removed cannot be covered by 2×1 dominoes. John McCarthy postulates that a mechanized system of heavy duty set theory should accept his formal description of the proposition and his proof that the covering is impossible, as presented at the qed meeting in Warsaw in 1995. This note is a report on solving the mutilated checkerboard problem in the Mizar proof checking environment.