Document Open Access Logo

Nine Chapters of Analytic Number Theory in Isabelle/HOL

Author Manuel Eberl

Thumbnail PDF


  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Manuel Eberl
  • Technical University of Munich, Boltzmannstraße 3, Garching bei München, Germany


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)


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
  • Isabelle
  • theorem proving
  • analytic number theory
  • number theory
  • arithmetical function
  • Dirichlet series
  • prime number theorem
  • Dirichlet’s theorem
  • zeta function
  • L functions


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail