From Weierstraß to Dedekind: Formalising Foundations of Modular Forms
by Manuel Eberl, Wenda Li, and Lawrence C. Paulson
In: Proceedings of ITP 2026 (to appear)
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 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 the ‘forbidden’ Eisenstein series G2.
In all of this, we aim for short and clean proofs, building a library of reusable lemmas.
Download preprint PDF (664 KiB)
BibTeX:
@inproceedings{elp26,
author="Eberl, Manuel and Li, Wenda and Paulson, Lawrence C.",
title="From Weierstraß to Dedekind: Formalising Foundations of Modular Forms",
year="To appear",
publisher="Leibniz International Proceedings in Informatics",
booktitle = "17th International Conference on Interactive Theorem Proving (ITP 2026)",
editor = "Komendantskaya, Ekaterina and Nipkow, Tobias",
address = "Dagstuhl, Germany",
sortyear="2026"
}