Nine chapters of analytic number theory in Isabelle/HOL. (English) Zbl 07649965
Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 16, 19 p. (2019).
Summary: 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:
For the entire collection see [Zbl 1423.68027].
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 \(\varphi(n)\).
For the entire collection see [Zbl 1423.68027].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
Keywords:
Isabelle; theorem proving; analytic number theory; number theory; arithmetical function; Dirichlet series; prime number theorem; Dirichlet’s theoremReferences:
| [1] | Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formalized Reasoning, 11(1):43-76, 2018. doi:10.6092/ issn.1972-5787/8124. · Zbl 1451.68329 · doi:10.6092/issn.1972-5787/8124 |
| [2] | Tom M. Apostol. Introduction to analytic number theory. Undergraduate Texts in Mathematics. Springer-Verlag, 1976. doi:10.1007/978-1-4757-5579-4. · Zbl 0335.10001 · doi: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. doi:10.1007/ 978-1-4612-0999-7. · Zbl 0697.10023 · doi: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. doi:10.6092/issn.1972-5787/3406. · Zbl 1451.68331 · doi: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. doi: 10.1145/1297658.1297660. · Zbl 1367.68244 · doi:10.1145/1297658.1297660 |
| [6] | Raymond Ayoub. Euler and the zeta function. The American Mathematical Monthly, 81(10):1067-1086, 1974. doi:10.2307/2319041. · Zbl 0293.10001 · doi:10.2307/2319041 |
| [7] | Joseph Bak and Donald J. Newman. Complex Analysis. Undergraduate Texts in Mathematics. Springer New York, 1999. |
| [8] | Clemens Ballarin. Locales: A Module System for Mathematical Theories. Journal of Automated Reasoning, 52(2):123-153, 2014. doi:10.1007/s10817-013-9284-7. · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7 |
| [9] | Julian Biendarra and Manuel Eberl. Bertrand’s postulate. Archive of Formal Proofs, Janu-ary 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. arXiv: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, Decem-ber 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. · Zbl 1467.68204 |
| [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. doi:10.6092/issn.1972-5787/1558. · Zbl 1205.68361 · doi: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. doi:10.1007/s10817-009-9145-6. · Zbl 1185.68624 · doi:10.1007/s10817-009-9145-6 |
| [21] | A. J. Hildebrand. Introduction to analytic number theory (lecture notes). https://faculty. math.illinois.edu/ hildebr/ant/. 16:19 |
| [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. doi:10.1007/978-3-642-39634-2_21. · Zbl 1317.68213 · doi: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. arXiv:1804. 03922. · Zbl 1468.68299 |
| [24] | M. Ram Murty and Marilyn Reece. A simple derivation of ζ(1 − K) = −BK /K. Funct. Approx. Comment. Math., 28:141-154, 2000. doi:10.7169/facm/1538186691. · Zbl 1034.11048 · doi:10.7169/facm/1538186691 |
| [25] | Donald J. Newman. Analytic number theory. Number 177 in Graduate Texts in Mathematics. Springer, 1998. doi:10.1007/b98872. · Zbl 0887.11001 · doi:10.1007/b98872 |
| [26] | Marco Riccardi. Pocklington’s theorem and Bertrand’s postulate. Formalized Mathematics, 14:47-52, January 2006. doi:10.2478/v10037-006-0007-y. · doi: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. doi:10.1007/10930755_20. · Zbl 1279.68298 · doi:10.1007/10930755_20 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
