Zagier一句证明的形式化验证
Formal verification of Zagier's one-sentence proof
摘要：
我们评论两个正式证明费马的两个平方和定理，书面使用的数学组件库的Coq证明助手。第一个遵循Zagier著名的一句话证明;第二个遵循David Christopher最近的证明依赖于分割理论的论点。这两种形式的证明依赖于一个一般性质的对合的有限集，独立的利益。证明技术主要包括通过特殊策略自动化经常性任务（例如自然数的大小写区分和计算）。用同样的方法，我们还给出了关于素数的另一个经典结果$a^2 + 2 b^2$的形式证明。
英文摘要：
We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's more recent proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics. With the same method, we also provide a formal proof of another classical result on primes of the form $a^2 + 2 b^2$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
