A formal proof of the irrationality of \(\zeta(3)\). (English) Zbl 07327949

Summary: 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.


03B70 Logic in computer science
68-XX Computer science
Full Text: arXiv Link


[1] Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis.J. Formalized Reasoning, 11(1):43-76, 2018. · Zbl 1451.68329
[2] Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff. A formally verified proof of the prime number theorem.ACM Trans. Comput. Logic, 9(1), December 2007. · Zbl 1367.68244
[3] Algolib.http://algo.inria.fr/libraries/, 2013. Version 17.0. For Maple 17. [Ap´e79]Roger Ap´ery. Irrationalit´e deζ(2) etζ(3).Ast´erisque, 61, 1979. Soci´et´e Math´ematique de France.
[4] Tom M. Apostol.Introduction to Analytic Number Theory. Undergraduate Texts in Mathematics. Springer, 1976. · Zbl 0335.10001
[5] Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub. Formal proofs of transcendence for e andπas an application of multivariate and symmetric polynomials.CoRR, abs/1512.02791, 2015.
[6] Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory.J. Funct. Program., 13(2):261-293, 2003. · Zbl 1060.03030
[7] Fr´ed´eric Besson. Fast reflexive arithmetic tactics the linear case and beyond. InTYPES’06, LNCS, pages 48-62, Berlin, Heidelberg, 2007. Springer-Verlag.
[8] F. Beukers. A note on the irrationality ofζ(2) andζ(3).Bull. London Math. Soc., 11(3):268-272, 1979. · Zbl 0421.10023
[9] Jesse Bingham. Formalizing a proof that e is transcendental.Journal of Formalized Reasoning, 4(1):71-84, 2011. · Zbl 1451.68317
[10] Keith Ball and Tanguy Rivoal. Irrationalit´e d’une infinit´e de valeurs de la fonction zˆeta aux entiers impairs.Invent. Math., 146(1):193-207, 2001. · Zbl 1058.11051
[11] Cyril Cohen, Maxime D´en‘es, and Anders M¨ortberg. Refinements for Free! InCertified Programs and Proofs, pages 147 - 162, Melbourne, Australia, December 2013.
[12] Fr´ed´eric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi. A ComputerAlgebra-Based Formal Proof of the Irrationality ofζ(3). InITP - 5th International Conference on Interactive Theorem Proving, Vienna, Austria, 2014. · Zbl 1416.68155
[13] Cyril Cohen. Construction of real algebraic numbers in Coq. InITP, volume 7406 ofLNCS. Springer, August 2012. · Zbl 1360.68744
[14] Mathematical Components Libraries.http://math-comp.github.io/math-comp/, 2019.
[15] David Delahaye and Micaela Mayero. Dealing with algebraic expressions over a field in Coq using Maple.J. Symb. Comput., 39(5):569-592, May 2005. · Zbl 1126.68101
[16] Manuel Eberl. The irrationality ofζ(3).Archive of Formal Proofs, December 2019.http: //isa-afp.org/entries/Zeta_3_Irrational.html, Formal proof development.
[17] Manuel Eberl. Nine chapters of analytic number theory in isabelle/hol. In John Harrison, John O’Leary, and Andrew Tolmach, editors,10th International Conference on Interactive Theorem · Zbl 1467.68204
[18] Bei-ye Feng. A simple elementary proof for the inequalitydn<3n.Acta Math. Appl. Sin. Engl. Ser., 21(3):455-458, 2005.
[19] St´ephane Fischler. Irrationalit´e de valeurs de zˆeta (d’apr‘es Ap´ery, Rivoal,. . .). InS´eminaire Bourbaki. Volume 2002/2003. Expos´es 909-923, pages 27-62, ex. Paris: Soci´et´e Math´ematique
[20] St´ephane Fischler, Johannes Sprang, and Wadim Zudilin. Many odd zeta values are irrational. Compositio Mathematica, 155(5):938-952, 2019. · Zbl 1430.11097
[21] Fran¸cois Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging Mathematical Structures. working paper or preprint, March 2009. · Zbl 1252.68253
[22] Benjamin Gr´egoire and Xavier Leroy. A compiled implementation of strong reduction. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, · Zbl 1322.68053
[23] Benjamin Gr´egoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. InTPHOLs 2005, volume 3603 ofLNCS, pages 98-113, Oxford, United Kingdom, August 2005. Springer. · Zbl 1152.68702
[24] Benjamin Gr´egoire, Laurent Th´ery, and Benjamin Werner.A Computational Approach to Pocklington Certificates in Type Theory, pages 97-113. Springer Berlin Heidelberg, Berlin, · Zbl 1185.68621
[25] Denis Hanson. On the product of the primes.Canad. Math. Bull., 15:33-37, 1972. · Zbl 0231.10008
[26] John Harrison. Formalizing an analytic proof of the Prime Number Theorem.Journal of Automated Reasoning, 43:243-261, 2009. · Zbl 1185.68624
[27] John Harrison. Formal proofs of hypergeometric sums (dedicated to the memory of andrzej trybulec).Journal of Automated Reasoning, 55:223-243, 2015. · Zbl 1356.68190
[28] Michael Hedberg. A coherence theorem for Martin-L¨of’s type theory.Journal of Functional Programming, 8(4):413-436, July 1998. · Zbl 0917.03028
[29] Florent Hivert. Coq-combi.https://github.com/hivert/Coq-Combi.
[30] Lars Hupel and Tobias Nipkow. A verified compiler from isabelle/hol to cakeml. In Amal Ahmed, editor,Programming Languages and Systems - 27th European Symposium on Programming, · Zbl 1418.68045
[31] John Harrison and L. Th´ery. A skeptic’s approach to combining HOL and Maple.J. Automat. Reason., 21(3):279-294, 1998. · Zbl 0916.68142
[32] Chantal Keller and Marc Lasson. Parametricity in an impredicative sort. In Patrick C´egielski and Arnaud Durand, editors,Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, · Zbl 1252.68259
[33] Assia Mahboubi and Enrico Tassi. Canonical Structures for the working Coq user. In Sandrine Blazy, Christine Paulin, and David Pichardie, editors,ITP 2013, 4th Conference on Interactive · Zbl 1317.68221
[34] Lo¨ıc Pottier. Connecting Gr¨obner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics.CoRR, abs/1007.3615, 2010.
[35] Tanguy Rivoal. La fonction zˆeta de Riemann prend une infinit´e de valeurs irrationnelles aux entiers impairs.C. R. Acad. Sci. Paris S´er. I Math., 331(4):267-270, 2000. · Zbl 0973.11072
[36] Bruno Salvy. An Algolib-aided version of Ap´ery’s proof of the irrationality ofζ(3).http: //algo.inria.fr/libraries/autocomb/Apery2-html/apery.html, 2003.
[37] Matthieu Sozeau. A new look at generalized rewriting in type theory.J. Formalized Reasoning, 2(1):41-62, 2009. · Zbl 1205.68364
[38] The Coq Development Team. The Coq Proof Assistant, version 8.11.0, January 2020.
[39] Nicolas Tabareau, ´Eric Tanter, and Matthieu Sozeau. Equivalences for free: univalent parametricity for effective transport.PACMPL, 2(ICFP):92:1-92:29, 2018.
[40] Alfred van der Poorten. A proof that Euler missed: Ap´ery’s proof of the irrationality ofζ(3). Math. Intelligencer, 1(4):195-203, 1979. An informal report. · Zbl 0409.10028
[41] Freek Wiedijk.The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence). Springer-Verlag New York, Inc., · Zbl 1126.68099
[42] Doron Zeilberger. A holonomic systems approach to special functions identities.J. Comput. Appl. Math., 32(3):321-368, 1990. · Zbl 0738.33001
[43] Doron Zeilberger. The method of creative telescoping.J. Symbolic Comput., 11(3):195-204, 1991. · Zbl 0738.33002
[44] V. V. Zudilin. One of the numbersζ(5),ζ(7),ζ(9),ζ(11) is irrational.Uspekhi Mat. Nauk, 56(4(340)):149-150, 2001.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.