The Riemann zeta function and Dirichlet L-functions are central objects in number theory, but their theory had only rudimentary formalization in Lean's Mathlib library, lacking key results like Dirichlet's theorem on primes in arithmetic progressions.

The authors formalize the theory of zeta and L-functions in Lean's Mathlib, building from an implementation of L-series through Fourier analysis connections to special values and applications. The formalization includes a proof of Dirichlet's theorem on primes in arithmetic progressions and a formal statement of the Riemann hypothesis. The work addresses challenges specific to formalization, such as handling totalizing functions in Lean.

The project contributes a formalization of Dirichlet's theorem on primes in arithmetic progressions and a formal statement of the Riemann hypothesis to Mathlib. The implementation provides reusable infrastructure for L-series that supports further number-theoretic formalization.