Nine Chapters of Analytic Number Theory in Isabelle/HOL

by Manuel Eberl

In: Proceedings of the 10th International Conference on Interactive Theorem Proving (Forthcoming)

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 ζ 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 σ₀(n), and Euler's totient function φ(n)

Download preprint PDF (526 KiB)

@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="Interactive Theorem Proving"
}

Download BibTeX (237 Bytes)