LIPIcs.ITP.2019.16.pdf
- Filesize: 0.54 MB
- 19 pages
Document
Nine Chapters of Analytic Number Theory in Isabelle/HOL
Author
Manuel Eberl 
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Author Details
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 AsGet 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
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)
0PDF Downloads