Assia Mahboubi ; Thomas Sibut-Pinote - A Formal Proof of the Irrationality of $\zeta(3)$

lmcs:5975 - Logical Methods in Computer Science, February 18, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:16)2021
A Formal Proof of the Irrationality of $\zeta(3)$Article

Authors: Assia Mahboubi ; Thomas Sibut-Pinote

    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éry 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.


    Volume: Volume 17, Issue 1
    Published on: February 18, 2021
    Accepted on: November 17, 2020
    Submitted on: December 16, 2019
    Keywords: Computer Science - Logic in Computer Science,F.3,F.3
    Funding:
      Source : OpenAIRE Graph
    • Fast Reliable Approximation; Funder: French National Research Agency (ANR); Code: ANR-14-CE25-0018

    Consultation statistics

    This page has been seen 1019 times.
    This article's PDF has been downloaded 799 times.