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

Frédéric Chyzak; Assia Mahboubi; Thomas Sibut-Pinote; Enrico Tassi

doi:10.1007/978-3-319-08970-6_11

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

Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer Verlag
Pages	160-176
Number of pages	17
ISBN (Print)	9783319089690
DOIs	https://doi.org/10.1007/978-3-319-08970-6_11
Publication status	Published - 1 Jan 2014
Externally published	Yes
Event	5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: 14 Jul 2014 → 17 Jul 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8558 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Country/Territory	Austria
City	Vienna
Period	14/07/14 → 17/07/14

Access to Document

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

Persistent URL (handle)

Persistent link

Cite this

Chyzak, F., Mahboubi, A., Sibut-Pinote, T., & Tassi, E. (2014). A computer-algebra-based formal proof of the irrationality of ζ(3). In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 160-176). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8558 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_11

Chyzak, Frédéric ; Mahboubi, Assia ; Sibut-Pinote, Thomas et al. / A computer-algebra-based formal proof of the irrationality of ζ(3). Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. pp. 160-176 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3b80d51007d942cc8a4f4cc0f84ba9aa,

title = "A computer-algebra-based formal proof of the irrationality of ζ(3)",

abstract = "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{\'e}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.",

author = "Fr{\'e}d{\'e}ric Chyzak and Assia Mahboubi and Thomas Sibut-Pinote and Enrico Tassi",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-319-08970-6_11",

language = "English",

isbn = "9783319089690",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "160--176",

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

address = "Germany",

note = "5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 14-07-2014 Through 17-07-2014",

}

Chyzak, F, Mahboubi, A, Sibut-Pinote, T & Tassi, E 2014, A computer-algebra-based formal proof of the irrationality of ζ(3). in Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8558 LNCS, Springer Verlag, pp. 160-176, 5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 14/07/14. https://doi.org/10.1007/978-3-319-08970-6_11

A computer-algebra-based formal proof of the irrationality of ζ(3). / Chyzak, Frédéric; Mahboubi, Assia; Sibut-Pinote, Thomas et al.
Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. p. 160-176 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8558 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

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 -

Chyzak F, Mahboubi A, Sibut-Pinote T, Tassi E. A computer-algebra-based formal proof of the irrationality of ζ(3). In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag. 2014. p. 160-176. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-08970-6_11

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

Abstract

Publication series

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this