  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.
