A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
Adrian De Lon, Koepke, Peter, Anton Lorenzen · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2021
Naproche is an emerging natural proof assistant that accepts input in a controlled natural language for mathematics, which we have integrated with LaTeX for ease of learning and to quickly produce high-quality typeset documents. We present a self-contained formalization of the Mutilated Checkerboard Problem in Naproche, following a proof sketch by John McCarthy. The formalization is embedded in detailed literate style comments. We also briefly describe the Naproche approach.