Document Open Access Logo

From Weierstraß to Dedekind via Jacobi: Formalising Foundations of Modular Forms

Authors Manuel Eberl , Wenda Li , Lawrence C. Paulson

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.23.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Isabelle/HOL
  • elliptic functions
  • Eisenstein series
  • modular forms
  • theta functions
  • number theory
  • complex analysis
  • formalisation of mathematics

Metrics

Abstract

We present an Isabelle/HOL formalisation of the foundations of analytic number theory related to modular forms. We begin by refactoring and extending the existing library on elliptic functions, adding the theorem that every elliptic function can be written in terms of the Weierstraß elliptic function ℘ and the addition theorem for ℘, which links complex lattices to elliptic curves. Next, we develop an extensive library on the Jacobi theta functions, including well-known results such as the Jacobi triple product, the Pentagonal Number Theorem, and the Rogers-Ramanujan identities. Finally, we apply this library to the study of the Dedekind η function and "forbidden" Eisenstein series G₂. In all of this, we aim for short and clean proofs, building a library of reusable lemmas.

Cite As Get BibTex

Manuel Eberl, Wenda Li, and Lawrence C. Paulson. From Weierstraß to Dedekind via Jacobi: Formalising Foundations of Modular Forms. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.23

Author Details

Manuel Eberl
  • University of Innsbruck, Austria
Wenda Li
  • University of Edinburgh, UK
Lawrence C. Paulson
  • University of Cambridge, UK

Acknowledgements

We would like to thank Alexey Ustinov for explaining how to prove an auxiliary lemma required for deriving the inversion formula for η from that for ϑ_{xy}, and George Andrews for clarifying an issue related to uniform convergence in the context of the Rogers-Ramanujan identities. Our thanks also go to Kristina Magnussen, who commented on a draft of this article, and to the anonymous reviewers.

Supplementary Materials

References

  1. G. E. Andrews and K. Eriksson. Integer Partitions. Cambridge University Press, 2004. Google Scholar
  2. George E. Andrews. A simple proof of Jacobi’s triple product identity. Proceedings of the American Mathematical Society, 16(2):333-334, April 1965. URL: https://doi.org/10.1090/s0002-9939-1965-0171725-x.
  3. Tom M. Apostol. Modular Functions and Dirichlet Series in Number Theory. Graduate Texts in Mathematics. Springer New York, 1990. URL: https://doi.org/10.1007/978-1-4612-0999-7.
  4. Clemens Ballarin. Locales: A module system for mathematical theories. Journal of Automated Reasoning, 52(2):123-153, April 2013. URL: https://doi.org/10.1007/s10817-013-9284-7.
  5. Richard Bellman. A Brief Introduction to Theta Functions. Holt, Rinehart and Winston, New York, 1961. Google Scholar
  6. Bruce C. Berndt. Ramanujan’s Notebooks. Springer New York, 1991. URL: https://doi.org/10.1007/978-1-4612-0965-2.
  7. Chris Birkbeck. Formalising modular forms, eisenstein series and the statement of the modularity conjecture. Preprint, available at https://cdbirkbeck.wixsite.com/website/research, 2023.
  8. Amine Chaieb. Formal power series. Journal of Automated Reasoning, 47(3):291-318, August 2010. URL: https://doi.org/10.1007/s10817-010-9195-9.
  9. Fred Diamond and Jerry Shurman. A First Course in Modular Forms. Springer New York, 2005. URL: https://doi.org/10.1007/978-0-387-27226-9.
  10. Manuel Eberl. Nine chapters of analytic number theory in Isabelle/HOL. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.16.
  11. Manuel Eberl. Verified real asymptotics in Isabelle/HOL. In Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC '19, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3326229.3326240.
  12. Manuel Eberl. A proof from THE BOOK: The partial fraction expansion of the cotangent. Archive of Formal Proofs, March 2022. Formal proof development. URL: https://isa-afp.org/entries/Cotangent_PFD_Formula.html.
  13. Manuel Eberl. Lambert series. Archive of Formal Proofs, November 2023. Formal proof development. URL: https://isa-afp.org/entries/Lambert_Series.html.
  14. Manuel Eberl. The polylogarithm function. Archive of Formal Proofs, November 2023. Formal proof development. URL: https://isa-afp.org/entries/Polylog.html.
  15. Manuel Eberl. Combinatorial q-analogues. Archive of Formal Proofs, December 2024. Formal proof development. URL: https://isa-afp.org/entries/Combinatorial_Q_Analogues.html.
  16. Manuel Eberl. The Rogers–Ramanujan identities. Archive of Formal Proofs, December 2024. Formal proof development. URL: https://isa-afp.org/entries/Rogers_Ramanujan.html.
  17. Manuel Eberl. Theta functions. Archive of Formal Proofs, December 2024. Formal proof development. URL: https://isa-afp.org/entries/Theta_Functions.html.
  18. Manuel Eberl. The partition function and the pentagonal number theorem. Archive of Formal Proofs, April 2025. Formal proof development. URL: https://isa-afp.org/entries/Pentagonal_Number_Theorem.html.
  19. Manuel Eberl, Anthony Bordg, Wenda Li, and Lawrence C. Paulson. Complex lattices, elliptic functions, and the modular group. Archive of Formal Proofs, May 2025. Formal proof development. URL: https://isa-afp.org/entries/Elliptic_Functions.html.
  20. Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Formalising half of a graduate textbook on number theory. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving (ITP 2024), pages 40:1-40:7, Dagstuhl, Germany, 2024. Leibniz International Proceedings in Informatics. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.40.
  21. Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Dedekind sums. Archive of Formal Proofs, April 2025. Formal proof development. URL: https://isa-afp.org/entries/Dedekind_Sums.html.
  22. John Harrison. Formalizing basic complex analysis. In R. Matuszewski and A. Zalewska, editors, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric, pages 151-165. University of Bialystok, 2007. Google Scholar
  23. John Harrison. Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). Journal of Automated Reasoning, 43(3):243-261, October 2009. URL: https://doi.org/10.1007/s10817-009-9145-6.
  24. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 279-294, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  25. Serge Lang. Elliptic Functions. Graduate Texts in Mathematics. Springer New York, 1973. URL: https://doi.org/10.1007/978-1-4612-4752-4.
  26. David Loeffler and Michael Stoll. Formalizing zeta and L-functions in lean. Annals of Formalized Mathematics, Volume 1, July 2025. URL: https://doi.org/10.46298/afm.15328.
  27. Carl Ludwig Siegel. A simple proof of η(-1/τ) = η(τ)√τ/i. Mathematika, 1(1):4, June 1954. URL: https://doi.org/10.1112/s0025579300000462.
  28. Jeremy Sylvestre. Formal Laurent series. Isabelle/HOL distribution, HOL-Computational_Algebra. Formal_Laurent_Series, 2019. Google Scholar
  29. The Isabelle Community. HOL-Complex_Analysis. Isabelle/HOL distribution, 2026. Google Scholar
  30. The mathlib community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, 2020. URL: https://doi.org/10.1145/3372885.3373824.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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