Formalising Half of a Graduate Textbook on Number Theory (Short Paper)

by Manuel Eberl, Anthony Bordg, Wenda Li, and Lawrence C. Paulson

In: Proceedings of ITP 2024

DOI:

10.4230/LIPIcs.ITP.2024.40

Abstract:

Apostol’s Modular Functions and Dirichlet Series in Number Theory is a graduate text covering topics such as elliptic functions, modular functions, approximation theorems and general Dirichlet series. It relies on complex analysis, winding numbers, the Riemann ζ function and Laurent series. We have formalised several chapters and can comment on the sort of gaps found in pedagogical mathematics.

Download preprint PDF (717 KiB)

BibTeX:

@inproceedings{eblp24,
  author="Eberl, Manuel and Bordg, Anthony and Paulson, Lawrence C. and Li, Wenda",
  title="Formalising Half of a Graduate Textbook on Number Theory",
  year="2024",
  publisher="Leibniz International Proceedings in Informatics",
  booktitle =	"15th International Conference on Interactive Theorem Proving (ITP 2024)",
  editor =	"Bertot, Yves and Kutsia, Temur and Norrish, Michael",
  address =	"Dagstuhl, Germany",
  doi =		"10.4230/LIPIcs.ITP.2024.40"
  pages =	"40:1--40:7"
}

Download BibTeX (505 Bytes)