Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture

TL;DR

This paper demonstrates how computer-assisted methods can successfully prove a complex combinatorial chess conjecture, showing the synergy of different approaches and the power of current technology in aiding human mathematical proofs.

Contribution

It provides a case study of computer support in proving a generalized chess endgame conjecture, illustrating the effectiveness of combined theorem proving approaches.

Findings

Confirmed a winning strategy for white in the generalized KRK endgame.

Showed the effectiveness of combining different computer theorem proving methods.

Established that current technology can significantly assist in complex mathematical proofs.

Abstract

There are several approaches for using computers in deriving mathematical proofs. For their illustration, we provide an in-depth study of using computer support for proving one complex combinatorial conjecture -- correctness of a strategy for the chess KRK endgame. The final, machine verifiable, result presented in this paper is that there is a winning strategy for white in the KRK endgame generalized to $n \times n$ board (for natural $n$ greater than $3$). We demonstrate that different approaches for computer-based theorem proving work best together and in synergy and that the technology currently available is powerful enough for providing significant help to humans deriving complex proofs.