Paper on formalizing analytic number theory

Stream: general

[David Loeffler]

Michael Stoll and I have just uploaded a preprint to the arXiv "Formalizing zeta and L-functions in Lean", arxiv:2503.00959

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."

We would be very grateful for any comments or feedback from this community.

[Notification Bot]

This topic was moved here from #general > Paper on formalising analytic number theory by David Loeffler.

[Filippo A. E. Nuccio]

Very nice paper, and great formalisation work! One very minor typo I spotted is on line 4 of Sec 6, where "donot" lacks a space.

[Michael Stoll]

@Filippo A. E. Nuccio Thanks! (This was already noticed in a DM by @Johan Commelin )

[Alex Kontorovich]

This is really a fantastic paper, great job @David Loeffler and @Michael Stoll!! I would love to see lots more such, which not only explain a significant chunk of the library in natural language, but also unpack a variety of design decisions, why one choice was made over others, and point to key theorems in the library. (Maybe such exist, in abundance already and I'm just ignorant?) I often stumble into a new part of Mathlib and am baffled by the design choices -- would it be possible to add, say, to the top of the Mathlib.NumberTheory.LSeries.Basicpage (and perhaps others), a link to this paper? Maybe that's something we can try to do more systematically -- link arxiv papers describing implementations to the Basic files in Mathlib? That could be a big boost for mathematicians unfamiliar with formalization (or even ones familiar but perhaps not with that part of the library!) trying to understand what's going on...

Some comments:
(1) Oops, the hyperlinks to hurwitzZetaEven and Odd are broken. So is LSeries_residueClass_eq. I get 404 errors.
(2) about theta series, how hard do you think it would now be to implement "general" theta series with arbitrary test functions (see, e.g., lecture 7 here: https://sites.math.rutgers.edu/~alexk/2023S572/index.html), even in the $G/\Gamma=\R/\Z$ case, and then derive the functional equations for even and odd Dirichlet series in one fell swoop? This could be a warmup for adelic Poisson summation and Tate's thesis... Also, the approach to getting Dirichlet characters from summing Hurwitz zeta functions doesn't generalize as easily to number fields; for Chebotarev, we'll want to be able to talk about group characters and develop the theory that way... Lots to discuss (maybe better over a zoom call sometime...)
(3) In section 3.3, you don't have hyperlinks to the "FE-pair" formalization, which could be useful.
(4) About the Gregory-Leibniz formula (which apparently was also known to Madhava some centuries earlier) and the footnote, I'm not sure what is meant that the method doesn't generalize? We have the Dirichlet class number formula, don't we? (And this is the special case with $\chi(\mod 4)$, as you say.) Oh maybe we don't; I looked briefly and didn't see it. Well, something else to pursue.
(5) Ha! Love seeing the comment "This one's for you, Kevin" in riemannZeta_one_ne_zero. And very important remark at the end of section 5!
(6) Does your proof of DirichletCharacter.LFunction_ne_zero_of_one_le_re appear in the literature somewhere? It was news to me (cool method!)

Again, congrats on a really fantastic paper (summarizing fantastic formalization work)!

[Michael Stoll]

Alex Kontorovich said:

(6) Does your proof of DirichletCharacter.LFunction_ne_zero_of_one_le_re appear in the literature somewhere? It was news to me (cool method!)

It is a variant of a fairly standard argument (compare, e.g., Thm. 2 in Section 16.5 of Ireland-Rosen, where instead of using $L(s,\chi) \zeta(s)$ they use $L(s,\chi)L(s,\chi_0)/L(2s,\chi_0)$, which vanishes at $s = 1/2$, so they only need the analytic continuation for $\operatorname{Re} s > 0$).

[Michael Stoll]

Alex Kontorovich said:

would it be possible to add, say, to the top of the Mathlib.NumberTheory.LSeries.Basicpage (and perhaps others), a link to this paper?

Sure. I'll prepare a PR adding a link to arXiv (which later can be replaced by a reference when the paper has appeared in a journal).

[Ruben Van de Velde]

Also enjoyed reading it, despite not having much of a clue about the mathematics :)

Good idea on linking it in the documentation, but maybe longer term we need to think about making room for such write-ups directly inside mathlib, so we can keep them up to date if needed?

[Michael Stoll]

#22599

[Kevin Buzzard]

Isn't the canonical thing to do to add it to the reference.bib file?

[Michael Stoll]

Yes, but maybe after it has appeared "properly"?

[Michael Stoll]

@Johan Commelin That may have been too early; CI has not yet finished...

[David Loeffler]

Hi Alex, thank you very much for your close reading of the paper and valuable comments! I'll fix all the broken links, etc, and upload a new version to the arxiv (there'll be the usual 24-hour delay).

[Ruben Van de Velde]

I don't think this needs CI that badly, and worst case bors rejects it in the end. But bors rejected it anyway :)

[Michael Stoll]

Yeah; I noticed the "rejected by label" comment.

[David Loeffler]

Re your questions:

Alex Kontorovich said:

(2) about theta series, how hard do you think it would now be to implement "general" theta series with arbitrary test functions (see, e.g., lecture 7 here: https://sites.math.rutgers.edu/~alexk/2023S572/index.html), even in the $G/\Gamma=\R/\Z$ case, and then derive the functional equations for even and odd Dirichlet series in one fell swoop?

Yes, something like that is surely doable. We didn't write it that way because the Schwartz class wasn't in Mathlib at the time; so I knew all the sums and integrals converged if the input function was a Gaussian, but didn't have a larger space to put it inside. Now, thanks to great work by many people, we do have a definition of the Schwartz class on $\mathbb{R}^2$ + proof it is preserved by the Fourier transform.

(An alternative would be to define theta series for Schwartz functions on the finite adeles (fixing the component at infinity), which is just a matter of taking suitable linear combinations of the Jacobi theta. It would be very easy to show, just a matter of unfolding definitions, that substituting $\tau \mapsto -1/\tau$ sends the theta function of $\Phi$ to that of $\widehat\Phi$. I kind of like this idea because it would give us lots of natural examples of modular forms. But I haven't sat down and tried to work it out properly.)

[Alex Kontorovich]

Michael Stoll said:

It is a variant of a fairly standard argument (compare, e.g., Thm. 2 in Section 16.5 of Ireland-Rosen, where instead of using $L(s,\chi) \zeta(s)$ they use $L(s,\chi)L(s,\chi_0)/L(2s,\chi_0)$, which vanishes at $s = 1/2$, so they only need the analytic continuation for $\operatorname{Re} s > 0$).

Sorry, I meant to link to LSeries.positive_of_differentiable_of_eqOn, that if a series has nonnegative coefficients and converges somewhere, then its continuation is strictly positive on the reals. (It bears some resemblance to Landau-type lemmas, but I don't recall seeing this fact isolated before.)

[Alex Kontorovich]

Michael Stoll said:

Sure. I'll prepare a PR adding a link to arXiv (which later can be replaced by a reference when the paper has appeared in a journal).

I personally even prefer arxiv! (I guess if it appears in a Diamond Open Access journal where one can similarly click one button and get the paper, that's just as good... :blush: )

[Michael Stoll]

The proof of the theorem in I-R I mentioned earlier goes via the same route: they observe that the L-series they consider has nonnegative coefficients (and $a_1 = 1$) and then use this to show that the higher derivatives at $s = 2$ alternate in sign, which implies that the function is positive (even $\ge 1$) left of $s = 2$.

[Alex Kontorovich]

Yes I recognize the method a posteriori, but hadn't seen this particular lemma isolated. It's nice!

[Michael Stoll]

That's what formalization tends to encourage: separate out useful statements as their own lemmas :smile:

[David Loeffler]

(4) About the Gregory-Leibniz formula (which apparently was also known to Madhava some centuries earlier) and the footnote, I'm not sure what is meant that the method doesn't generalize? We have the Dirichlet class number formula, don't we? (And this is the special case with $χ(mod4)$, as you say.) Oh maybe we don't; I looked briefly and didn't see it. Well, something else to pursue.

This was a last-minute addition to the paper so it's possible I overlooked something. AFAIK, we don't have the Dirichlet class number formula just yet, although @Xavier Roblot is getting pretty close! The proof we have for Gregory-Leibniz relies on having the explicit form $\sum (-1)^n x^{2n+1}/(2n + 1) = arctan x$ for $|x| < 1$ and taking a limit as $x \to 1$ which (AFAIK) does not generalize to other Dirichlet L-series.

[Alex Kontorovich]

Right, and if you'd already had the class number formula, you wouldn't have needed to prove $L(\chi,1)\ne0$... :)

[Michael Stoll]

Alex Kontorovich said:

I personally even prefer arxiv!

We can certainly include the arXiv link with the entry when we add it.

[Xavier Roblot]

David Loeffler said:

This was a last-minute addition to the paper so it's possible I overlooked something. AFAIK, we don't have the Dirichlet class number formula just yet, although Xavier Roblot is getting pretty close! The proof we have for Gregory-Leibniz relies on having the explicit form $\sum (-1)^n x^{2n+1}/(2n + 1) = arctan x$ for $|x| < 1$ and taking a limit as $x \to 1$ which (AFAIK) does not generalize to other Dirichlet L-series.

The proof of Dirichlet class number formula is complete and is here: #17914. It is getting slowly into Mathlib

[David Loeffler]

Xavier Roblot said:

The proof of Dirichlet class number formula is complete and is here: #17914. It is getting slowly into Mathlib

This would give formulae for $L(\chi, 0)$ for odd quadratic $\chi$, and $L'(\chi, 0)$ for nontrivial even quadratic chi; but it wouldn't give you the exact values for higher-order characters, would it? You can't separate out terms for different characters with the same splitting field.

[Alex Kontorovich]

Xavier Roblot said:

The proof of Dirichlet class number formula is complete and is here: #17914. It is getting slowly into Mathlib

Wow, this is amazing! So we're much closer to Chebotarev than I'd thought! I have to step on the gas on my end...

[Alex Kontorovich]

Is anyone working on specializing to the case $K={\mathbb Q}(\sqrt D)$ to go full circle to Dirichlet characters and $L$-functions?