2026-07-20T07:45:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11071 2024-03-06T10:47:17Z ddc:004 open_access

Nine Chapters of Analytic Number Theory in Isabelle/HOL Eberl, Manuel Isabelle theorem proving analytic number theory number theory arithmetical function Dirichlet series prime number theorem Dirichlet’s theorem zeta function L functions 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) Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manuel Eberl 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.16 urn:nbn:de:0030-drops-110714 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.16 eng https://creativecommons.org/licenses/by/3.0/legalcode