Nine Chapters of Analytic Number Theory in Isabelle/HOL
by Manuel Eberl
In: Proceedings of ITP 2019
DOI:
10.4230/LIPIcs.ITP.2019.16Abstract:
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 ζ 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 ω function, the divisor count σ0(n), and Euler's totient function φ(n)
Download preprint PDF (526 KiB)
BibTeX:
@inproceedings{eberl19ant,
author="Eberl, Manuel",
title="Nine Chapters of Analytic Number Theory in {I}sabelle/{HOL}",
year="2019",
publisher="Leibniz International Proceedings in Informatics",
booktitle = "10th International Conference on Interactive Theorem Proving (ITP 2019)",
pages = "16:1--16:19",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
ISBN = "978-3-95977-122-1",
ISSN = "1868-8969",
volume = "141",
editor = "John Harrison and John O'Leary and Andrew Tolmach",
publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
address = {"Dagstuhl, Germany"
}