eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
16:1
16:19
10.4230/LIPIcs.ITP.2019.16
article
Nine Chapters of Analytic Number Theory in Isabelle/HOL
Eberl, Manuel
1
https://orcid.org/0000-0002-4263-6571
Technical University of Munich, Boltzmannstraße 3, Garching bei München, Germany
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)
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.16/LIPIcs.ITP.2019.16.pdf
Isabelle
theorem proving
analytic number theory
number theory
arithmetical function
Dirichlet series
prime number theorem
Dirichlet’s theorem
zeta function
L functions