Formalizing zeta and L-functions in Lean
Number Theory
2025-07-16 v4 Formal Languages and Automata Theory
Logic in Computer Science
Abstract
The Riemann zeta function, and more generally the L-functions of Dirichlet characters, are among the central objects of study in number theory. We report on a project to formalize the theory of these objects in Lean's "Mathlib" library, including a proof of Dirichlet's theorem on primes in arithmetic progressions and a formal statement of the Riemann hypothesis
Cite
@article{arxiv.2503.00959,
title = {Formalizing zeta and L-functions in Lean},
author = {David Loeffler and Michael Stoll},
journal= {arXiv preprint arXiv:2503.00959},
year = {2025}
}
Comments
Final version, to appear in Annals of Formalized Mathematics