José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. arxiv.org/abs/2503.00959

arXiv logo

Formalizing zeta and L-functions in Lean

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

arxiv.org · arXiv.org

0
0
0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/Jose_A_Alonso/statuses/114675535043007807 on your instance and quote it. (Note that quoting is not supported in Mastodon.)