扎吉尔一句话证明的形式化验证

我们评述了使用 Coq 证明助手的 Mathematical Components 库所写的两个费马两平方和定理的形式化证明。第一个遵循扎吉尔(Zagier)著名的一句话证明；第二个遵循 David Christopher 近期基于分拆理论论证的证明。两个形式化证明都依赖于有限集对合的一个具有独立意义的一般性质。证明技术在很大程度上在于通过专用策略自动化重复任务（如分情况讨论与自然数的计算）。运用同一方法，我们还给出了形如 $a^2 + 2 b^2$ 的素数另一经典结果的形式化证明。