Document Open Access Logo

Nine Chapters of Analytic Number Theory in Isabelle/HOL

Author Manuel Eberl

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.16.pdf
  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Manuel Eberl
  • Technical University of Munich, Boltzmannstraße 3, Garching bei München, Germany

Funding

This work was supported by DFG grant NI 491/16-1. Part of it was conducted during a research visit in collaboration with the ALEXANDRIA project (ERC grant 742178).

Acknowledgements

I would like to thank John Harrison for doing all the incredibly hard work of creating an extensive library of complex analysis in HOL Light - the first of its kind - and Larry Paulson and Wenda Li for porting it to Isabelle/HOL and extending it even further. Without these efforts, my work would not have been possible. Larry Paulson also started off the analytic proof of the Prime Number Theorem in Isabelle and allowed me to take over and replace it with a more high-level approach. I also thank Jeremy Avigad and Johannes Hölzl, who commented on a draft of this document, and the anonymous reviewers, who gave a number of helpful suggestions.

Cite As Get BibTex

Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.16

Abstract

In this paper, I present a formalisation of a large portion of Apostol’s Introduction to Analytic Number Theory in Isabelle/HOL. Of the 14 chapters in the book, the content of 9 has been mostly formalised, while the content of 3 others was already mostly available in Isabelle before.
The most interesting results that were formalised are: 
- The Riemann and Hurwitz zeta functions and the Dirichlet L functions 
- Dirichlet’s theorem on primes in arithmetic progressions 
- An analytic proof of the Prime Number Theorem 
- The asymptotics of arithmetical functions such as the prime omega function, the divisor count sigma_0(n), and Euler’s totient function phi(n)

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Mathematical analysis
Keywords
  • Isabelle
  • theorem proving
  • analytic number theory
  • number theory
  • arithmetical function
  • Dirichlet series
  • prime number theorem
  • Dirichlet’s theorem
  • zeta function
  • L functions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

  • The proof developments in the Archive of Formal Proofs (AFP) that this work refers to are listed in the bibliography. Additionally, a precise overview of what material from the book has been formalised and which theorems in the book correspond to which theorems in the formalisation can be found at https://doi.org/10.5281/zenodo.3262266.

References

  1. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formalized Reasoning, 11(1):43-76, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8124.
  2. Tom M. Apostol. Introduction to analytic number theory. Undergraduate Texts in Mathematics. Springer-Verlag, 1976. URL: https://doi.org/10.1007/978-1-4757-5579-4.
  3. Tom M. Apostol. Modular Functions and Dirichlet Series in Number Theory, volume 41 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1990. URL: https://doi.org/10.1007/978-1-4612-0999-7.
  4. Andrea Asperti and Wilmer Ricciotti. A proof of Bertrand’s postulate. Journal of Formalized Reasoning, 5(1):37-57, 2012. URL: https://doi.org/10.6092/issn.1972-5787/3406.
  5. 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. URL: https://doi.org/10.1145/1297658.1297660.
  6. Raymond Ayoub. Euler and the zeta function. The American Mathematical Monthly, 81(10):1067-1086, 1974. URL: https://doi.org/10.2307/2319041.
  7. Joseph Bak and Donald J. Newman. Complex Analysis. Undergraduate Texts in Mathematics. Springer New York, 1999. Google Scholar
  8. Clemens Ballarin. Locales: A Module System for Mathematical Theories. Journal of Automated Reasoning, 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  9. Julian Biendarra and Manuel Eberl. Bertrand’s postulate. Archive of Formal Proofs, January 2017. , Formal proof development. URL: http://isa-afp.org/entries/Bertrands_Postulate.html.
  10. Mario Carneiro. Arithmetic in Metamath, Case Study: Bertrand’s Postulate. CoRR, abs/1503.02349, 2015. URL: http://arxiv.org/abs/1503.02349.
  11. Mario Carneiro. Formalization of the prime number theorem and Dirichlet’s theorem. In Proceedings of the 9th Conference on Intelligent Computer Mathematics (CICM 2016), pages 10-13, 2016. URL: http://ceur-ws.org/Vol-1785/F3.pdf.
  12. Manuel Eberl. Dirichlet L-functions and Dirichlet’s theorem. Archive of Formal Proofs, December 2017. , Formal proof development. URL: http://isa-afp.org/entries/Dirichlet_L.html.
  13. Manuel Eberl. Dirichlet series. Archive of Formal Proofs, October 2017. , Formal proof development. URL: http://isa-afp.org/entries/Dirichlet_Series.html.
  14. Manuel Eberl. The Euler–MacLaurin Formula. Archive of Formal Proofs, March 2017. , Formal proof development. URL: http://isa-afp.org/entries/Euler_MacLaurin.html.
  15. Manuel Eberl. The Hurwitz and Riemann ζ Functions. Archive of Formal Proofs, October 2017. , Formal proof development. URL: http://isa-afp.org/entries/Zeta_Function.html.
  16. Manuel Eberl. Elementary Facts About the Distribution of Primes. Archive of Formal Proofs, February 2019. , Formal proof development. URL: http://isa-afp.org/entries/Prime_Distribution_Elementary.html.
  17. Manuel Eberl. Verified Real Asymptotics in Isabelle/HOL. Draft available at https://www21.in.tum.de/~eberlm/real_asymp.pdf, 2019.
  18. Manuel Eberl and Lawrence C. Paulson. The Prime Number Theorem. Archive of Formal Proofs, September 2018. , Formal proof development. URL: http://isa-afp.org/entries/Prime_Number_Theorem.html.
  19. John Harrison. A formalized proof of Dirichlet’s theorem on primes in arithmetic progression. Journal of Formalized Reasoning, 2(1):63-83, 2009. URL: https://doi.org/10.6092/issn.1972-5787/1558.
  20. John Harrison. Formalizing an analytic proof of the Prime Number Theorem (Dedicated to Mike Gordon on the occasion of his 60th birthday). Journal of Automated Reasoning, 43(3):243-261, October 2009. URL: https://doi.org/10.1007/s10817-009-9145-6.
  21. A. J. Hildebrand. Introduction to analytic number theory (lecture notes). URL: https://faculty.math.illinois.edu/~hildebr/ant/.
  22. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, volume 7998 of Lecture Notes in Computer Science, pages 279-294. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  23. Wenda Li and Lawrence C. Paulson. Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL. CoRR, abs/1804.03922, 2018. URL: http://arxiv.org/abs/1804.03922.
  24. M. Ram Murty and Marilyn Reece. A simple derivation of ζ(1-K) = -B_K/K. Funct. Approx. Comment. Math., 28:141-154, 2000. URL: https://doi.org/10.7169/facm/1538186691.
  25. Donald J. Newman. Analytic number theory. Number 177 in Graduate Texts in Mathematics. Springer, 1998. URL: https://doi.org/10.1007/b98872.
  26. Marco Riccardi. Pocklington’s theorem and Bertrand’s postulate. Formalized Mathematics, 14:47-52, January 2006. URL: https://doi.org/10.2478/v10037-006-0007-y.
  27. Laurent Théry. Proving Pearl: Knuth’s Algorithm for Prime Numbers. In David Basin and Burkhart Wolff, editors, Theorem Proving in Higher Order Logics, pages 304-318, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/10930755_20.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact