Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Nine Chapters of Analytic Number Theory in Isabelle/HOL

by Manuel Eberl

In: Proceedings of ITP 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:

Download preprint PDF (526 KiB)


  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"

Download BibTeX (542 Bytes)