DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.23

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

Authors: Manuel Eberl, Wenda Li, and Lawrence C. Paulson

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{eberl_et_al:LIPIcs.ITP.2026.23,
  author =	{Eberl, Manuel and Li, Wenda and Paulson, Lawrence C.},
  title =	{{From Weierstra{\ss} to Dedekind via Jacobi: Formalising Foundations of Modular Forms}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.23},
  URN =		{urn:nbn:de:0030-drops-269976},
  doi =		{10.4230/LIPIcs.ITP.2026.23},
  annote =	{Keywords: Isabelle/HOL, elliptic functions, Eisenstein series, modular forms, theta functions, number theory, complex analysis, formalisation of mathematics}
}

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2026.32

Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)

Authors: Aeacus Sheng, Wenda Li, and Paul B. Jackson

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes' rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm's theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches. We take an initial step towards efficient verified real root isolation by formally verifying two simple algorithms based on Descartes' rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms, present formal proofs of termination, soundness, and completeness, and discuss our code-generation efforts. Brief experiments show promising performance improvements over existing formally verified algorithms in Isabelle/HOL.

Cite as

Aeacus Sheng, Wenda Li, and Paul B. Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 32:1-32:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.ITP.2026.32,
  author =	{Sheng, Aeacus and Li, Wenda and Jackson, Paul B.},
  title =	{{Faster Verified Real Root Isolation with Descartes' Rule of Signs}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{32:1--32:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.32},
  URN =		{urn:nbn:de:0030-drops-270068},
  doi =		{10.4230/LIPIcs.ITP.2026.32},
  annote =	{Keywords: Isabelle/HOL, Real root isolation, Descartes' rule of signs}
}

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2024.40

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

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

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{eberl_et_al:LIPIcs.ITP.2024.40,
  author =	{Eberl, Manuel and Bordg, Anthony and Paulson, Lawrence C. and Li, Wenda},
  title =	{{Formalising Half of a Graduate Textbook on Number Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{40:1--40:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.40},
  URN =		{urn:nbn:de:0030-drops-207686},
  doi =		{10.4230/LIPIcs.ITP.2024.40},
  annote =	{Keywords: Isabelle/HOL, number theory, complex analysis, formalisation of mathematics}
}

Search Results

Documents authored by Li, Wenda

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

Abstract

Cite as

Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)

Abstract

Cite as

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

Abstract

Cite as

Thanks for your feedback!

Could not send message