A Formal Proof of the Irrationality of $\zeta(3)$

TL;DR

This paper provides a fully formalized proof of the irrationality of ζ(3) using the Coq proof assistant, verifying Apéry's original proof with computer algebra and extended mathematical libraries.

Contribution

It is the first complete formal verification of Apéry's proof of ζ(3)'s irrationality, integrating computer algebra verification within a proof assistant.

Findings

Formal proof of ζ(3) irrationality completed in Coq

Verification of computer algebra calculations included

Extended mathematical libraries support the proof

Abstract

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.