Formalizing zeta and L-functions in Lean

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

Final version, to appear in Annals of Formalized Mathematics