Authors: Predrag Janičić ; Filip Marić ; Marko Maliković

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.

• 03B35 - Mechanization of proofs and logical operations
• 68V15 - Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
• 91A46 - Combinatorial games