一句话：用机器可验证方法证明 n×n 棋盘扩展 KRK 残局白方必胜，并展示多种计算机证明方法的协同。
本文研究如何用计算机辅助证明有限域上的组合猜想，并以国际象棋 KRK 残局的策略正确性作为复杂案例进行深入分析。作者综合运用多种计算机定理证明方法，协同构建证明，最终得到机器可验证的结果：在推广到 n×n 棋盘（自然数 n>3）的 KRK 残局中，白方存在必胜策略。案例表明，不同计算机证明途径相互结合效果最佳，且现有技术已能为人类推导复杂证明提供重要帮助。该工作展示了计算机辅助证明在组合猜想验证中的可行性与协同价值。
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.
@article{paperbot810,
title = {Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture},
author = {Predrag Janičić and Filip Marić and Marko Maliković},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:34)2019}
}