一句话：在 Coq 中完整形式化了 Apéry 关于 ζ(3) 无理性的证明，并验证了计算机代数计算。
本文报告在 Coq 证明助手中完成 Riemann zeta 函数在 3 处取值 ζ(3) 无理性的形式验证。证明沿 Apéry 于 1978 年给出的原始路线，核心是证明若干序列满足共同递推关系。作者通过对 Maple 会话中计算机代数算法执行的计算进行事后验证，形式化了这一关键步骤；证明的其余部分结合算术论证与渐近分析，并通过扩展 Mathematical Components 库来完成。最终得到该经典数论结果的完整机器检验证明。
This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Ap\'ery in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.
@article{paperbot1335,
title = {A Formal Proof of the Irrationality of $\zeta(3)$},
author = {Assia Mahboubi and Thomas Sibut-Pinote},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:16)2021}
}