LIPIcs.ITP.2024.40.pdf
- Filesize: 0.7 MB
- 7 pages
Document
Formalising Half of a Graduate Textbook on Number Theory (Short Paper)
Authors
Manuel Eberl 
,
Anthony Bordg ,
Lawrence C. Paulson ,
Wenda Li
-
Part of:
Volume:
15th International Conference on Interactive Theorem Proving (ITP 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-09-02
File
Document Identifiers
Author Details
- Université Paris-Saclay, INRIA, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, France
Acknowledgements
We would like to thank Sander Dahmen and Kevin Buzzard for providing various advice concerning number theory and the reviewers for their suggestions.
Cite As Get BibTex
Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Formalising Half of a Graduate Textbook on Number Theory (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 40:1-40:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.40
Abstract
Apostol’s Modular Functions and Dirichlet Series in Number Theory [Tom M. Apostol, 1990] 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. Proofs are available from https://github.com/Wenda302/Number_Theory_ITP2024.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Isabelle/HOL
- number theory
- complex analysis
- formalisation of mathematics
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Tom M. Apostol. Introduction to Analytic Number Theory. Springer, 1976.
-
Tom M. Apostol. Modular Functions and Dirichlet Series in Number Theory. Springer, 1990.
- Chris Birkbeck. ModularForms. GitHub repository. URL: https://github.com/CBirkbeck/ModularForms.
-
Manuel Eberl. Nine chapters of analytic number theory in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:19, 2019.
- Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Formalising half of a graduate textbook on number theory (formal proof development), June 2024. URL: https://doi.org/10.5281/zenodo.12586104.
- Norbert Hungerbühler and Micha Wasem. Non-integer valued winding numbers and a generalized residue theorem. Journal of Mathematics, 2019:1-9, March 2019. URL: https://doi.org/10.1155/2019/6130464.
-
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002.
-
L. S. van Benthem Jutting. Checking Landau’s "Grundlagen" in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977.