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

DOI: 10.4230/LIPIcs.ITP.2025.35

Verifying an Efficient Algorithm for Computing Bernoulli Numbers

Authors: Manuel Eberl and Peter Lammich

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

The Bernoulli numbers B_k are a sequence of rational numbers that is ubiquitous in mathematics, but difficult to compute efficiently (compared to e.g. approximating π). In 2008, Harvey gave the currently fastest known practical way for computing them: his algorithm computes B_k mod p in time O(p log^{1 + o(1)} p). By doing this for O(k) many small primes p in parallel and then combining the results with the Chinese Remainder Theorem, one recovers the value of B_k as a rational number in O(k² log^{2 + o(1)} k) time. One advantage of this approach is that the expensive part of the algorithm is highly parallelisable and has very low memory requirements. This algorithm still holds the world record with its computation of B_{10⁸}. We give a verified efficient LLVM implementation of this algorithm. This was achieved by formalising the necessary mathematical background theory in Isabelle/HOL, proving an abstract version of the algorithm correct, and refining this abstract version down to LLVM using Lammich’s Isabelle-LLVM framework, including many low-level optimisations. The performance of the resulting LLVM code is comparable with Harvey’s original unverified and hand-optimised C++ implementation.

Cite as

Manuel Eberl and Peter Lammich. Verifying an Efficient Algorithm for Computing Bernoulli Numbers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{eberl_et_al:LIPIcs.ITP.2025.35,
  author =	{Eberl, Manuel and Lammich, Peter},
  title =	{{Verifying an Efficient Algorithm for Computing Bernoulli Numbers}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.35},
  URN =		{urn:nbn:de:0030-drops-246331},
  doi =		{10.4230/LIPIcs.ITP.2025.35},
  annote =	{Keywords: Bernoulli numbers, LLVM, verification, Isabelle, Chinese remainder theorem, modular arithmetic, Montgomery arithmetic}
}

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}
}

Document

DOI: 10.4230/LIPIcs.ITP.2019.16

Nine Chapters of Analytic Number Theory in Isabelle/HOL

Authors: Manuel Eberl

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract

In this paper, I present a formalisation of a large portion of Apostol’s Introduction to Analytic Number Theory in Isabelle/HOL. Of the 14 chapters in the book, the content of 9 has been mostly formalised, while the content of 3 others was already mostly available in Isabelle before. The most interesting results that were formalised are: - The Riemann and Hurwitz zeta functions and the Dirichlet L functions - Dirichlet’s theorem on primes in arithmetic progressions - An analytic proof of the Prime Number Theorem - The asymptotics of arithmetical functions such as the prime omega function, the divisor count sigma_0(n), and Euler’s totient function phi(n)

Cite as

Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{eberl:LIPIcs.ITP.2019.16,
  author =	{Eberl, Manuel},
  title =	{{Nine Chapters of Analytic Number Theory in Isabelle/HOL}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.16},
  URN =		{urn:nbn:de:0030-drops-110714},
  doi =		{10.4230/LIPIcs.ITP.2019.16},
  annote =	{Keywords: Isabelle, theorem proving, analytic number theory, number theory, arithmetical function, Dirichlet series, prime number theorem, Dirichlet’s theorem, zeta function, L functions}
}

Search Results

Documents authored by Eberl, Manuel

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

Abstract

Cite as

Verifying an Efficient Algorithm for Computing Bernoulli Numbers

Abstract

Cite as

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

Abstract

Cite as

Nine Chapters of Analytic Number Theory in Isabelle/HOL

Abstract

Cite as

Thanks for your feedback!

Could not send message