Document Open Access Logo

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

Authors Manuel Eberl , Anthony Bordg , Lawrence C. Paulson , Wenda Li

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.40.pdf
  • Filesize: 0.7 MB
  • 7 pages

Document Identifiers

Author Details

Manuel Eberl
  • University of Innsbruck, Austria
Anthony Bordg
  • Université Paris-Saclay, INRIA, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, France
Lawrence C. Paulson
  • University of Cambridge, UK
Wenda Li
  • University of Edinburgh, UK

Funding

ERC Advanced Grant ALEXANDRIA (Project 742178).

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 AsGet 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)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Tom M. Apostol. Introduction to Analytic Number Theory. Springer, 1976. Google Scholar
  2. Tom M. Apostol. Modular Functions and Dirichlet Series in Number Theory. Springer, 1990. Google Scholar
  3. Chris Birkbeck. ModularForms. GitHub repository. URL: https://github.com/CBirkbeck/ModularForms.
  4. 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. Google Scholar
  5. 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.
  6. 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.
  7. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002. Google Scholar
  8. L. S. van Benthem Jutting. Checking Landau’s "Grundlagen" in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact