Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Nine Chapters of Analytic Number Theory in Isabelle/HOL

by Manuel Eberl

In: Proceedings of the 10th International Conference on Interactive Theorem Proving (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 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)

BibTeX:

@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 =	"10th International Conference on Interactive Theorem Proving (ITP 2019)",
pages =	"16:1--16:19",
series =	"Leibniz International Proceedings in Informatics (LIPIcs)",
ISBN =	"978-3-95977-122-1",
ISSN =	"1868-8969",
volume =	"141",
editor =	"John Harrison and John O'Leary and Andrew Tolmach",
publisher =	"Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
address =	{"Dagstuhl, Germany"
}

Download BibTeX (600 Bytes)