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.

翻译：本文用Coq 校对助理对Riemann zeta 3 的函数评价是非理性的。 这个结果首先由 Ap\'ery 于1978年提出,我们正式确定的证据基本上遵循他最初的表述方式。 这个证据的症结在于确定某些序列符合常见的重现。 我们通过在Maple 会话中对计算机代数算法进行的计算进行事后核查来正式证明这一结果。 其余的证明结合了计算成份和无症状分析, 我们通过扩展数学构件库来进行这种分析。