Authors: David Loeffler ; Michael Stoll

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

• 11M06 - \(\zeta (s)\) and \(L(s, \chi)\)
• 68V20 - Formalization of mathematics in connection with theorem provers