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 proceedingConference contributionAcademicpeer-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 languageEnglish
Title of host publicationInteractive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer Verlag
Pages160-176
Number of pages17
ISBN (Print)9783319089690
DOIs
Publication statusPublished - 1 Jan 2014
Externally publishedYes
Event5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: 14 Jul 201417 Jul 2014

Publication series

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

Conference

Conference5th International Conference on Interactive Theorem Proving, ITP 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period14/07/1417/07/14

Fingerprint

Dive into the research topics of 'A computer-algebra-based formal proof of the irrationality of ζ(3)'. Together they form a unique fingerprint.

Cite this