有限域上组合猜想的计算机辅助证明：一个国际象棋猜想的案例研究
Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture
AI总结：
本文以国际象棋KRK残局策略正确性证明为例，展示多种计算机辅助定理证明方法协同工作，最终机器验证了在$n \ imes n$棋盘（$n>3$）上白方存在必胜策略，表明现有技术能显著辅助人类推导复杂证明。
摘要：
在利用计算机推导数学证明方面有几种方法。为了说明这些方法，我们深入研究了如何利用计算机支持来证明一个复杂的组合猜想——国际象棋KRK残局中一个策略的正确性。本文呈现的最终机器可验证的结果是：在推广到$n \ imes n$棋盘（对于大于3的自然数$n$）的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
