# Nine Chapters of Analytic Number Theory in Isabelle/HOL

by Manuel Eberl

In: *Proceedings of ITP 2019*

### DOI:

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 Theoryin 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 DirichletLfunctions- 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σ, and Euler's totient function_{0}(n)φ(n)

Download preprint PDF (526 KiB)

### BibTeX:

```
@inproceedings{eberl19ant,
author = "Eberl, Manuel",
editor = "John Harrison and John O'Leary and Andrew Tolmach",
title = "Nine Chapters of Analytic Number Theory in {I}sabelle/{HOL}",
year = "2019",
booktitle = "Interactive Theorem Proving, {ITP} 2019",
pages = "16:1--16:19",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
doi = "10.4230/LIPIcs.ITP.2019.16",
ISBN = "978-3-95977-122-1",
ISSN = "1868-8969",
volume = "141",
publisher = "Schloss Dagstuhl, Leibniz-Zentrum f\"{u}r Informatik"
}
```