TY - GEN

T1 - A computer-algebra-based formal proof of the irrationality of ζ(3)

AU - Chyzak, Frédéric

AU - Mahboubi, Assia

AU - Sibut-Pinote, Thomas

AU - Tassi, Enrico

PY - 2014/1/1

Y1 - 2014/1/1

N2 - This paper describes the formal verification of an irrationality proof of ζ(3), the evaluation of the Riemann zeta function, using the Coq proof assistant. This result was first proved by Apéry in 1978, and the proof we have formalized 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 some asymptotic analysis that we conduct by extending the Mathematical Components libraries. The formalization of this proof is complete up to a weak corollary of the Prime Number Theorem.

AB - This paper describes the formal verification of an irrationality proof of ζ(3), the evaluation of the Riemann zeta function, using the Coq proof assistant. This result was first proved by Apéry in 1978, and the proof we have formalized 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 some asymptotic analysis that we conduct by extending the Mathematical Components libraries. The formalization of this proof is complete up to a weak corollary of the Prime Number Theorem.

UR - http://www.scopus.com/inward/record.url?scp=84904793488&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84904793488&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-08970-6_11

DO - 10.1007/978-3-319-08970-6_11

M3 - Conference contribution

AN - SCOPUS:84904793488

SN - 9783319089690

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 160

EP - 176

BT - Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

T2 - 5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014

Y2 - 14 July 2014 through 17 July 2014

ER -