Update

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

Hi all! Since successfully finishing WeakPNT, there has been a lot of good and steady progress on the project (much of it thanks to @Vláďa Sedláček) which I realize is not getting documented here on zulip. In particular, we’re getting closer to MediumPNT with an error savings of $\exp(c (\log x)^{1/10})$. Originally I had proposed to also prove an even stronger error which saves the “classical” $\exp(c (\log x)^{1/2})$, but the method I had in mind would involve developing a lot more complex analysis (e.g., something like Hadamard factorization), which now seems too much of a detour from our larger goal (Chebotarev).

Then a few weeks ago, I learned (thanks to Manuel Eberl) that there was a brand new formalization in Isabelle of the classical error! See: https://github.com/mmew-2022/Isabelle_Prime_Number_Theorem. I’ve been trying to “informalize” this formalization to figure out how exactly it was done (there are so many possibilities, each with their own technical advantages and difficulties), but have not yet succeeded. (If someone who knows Isabelle well could explain it to me, I would be grateful!)

Anyway, so at this point, I will refactor MediumPNT to be “modular”, to allow for any quality error, corresponding to whatever quality zero-free region can be obtained. It’ll take a few more days, and then I’ll post a new list of Outstanding Tasks. Thanks again for everyone’s help and contributions!!!

[Yuyang Zhao]

cc @Meow who made the formalization in Isabelle

[Alex Kontorovich]

Ah thanks! I didn't know who the Isabelle author was, and certainly didn't realize they were on here!

@Meow, I'd love to hop on a quick zoom call, if you get this and are available...? Please DM me

[Yuyang Zhao]

I asked about it today. She said it was using Theorem 3.10 of Titchmarsh's The theory of the Riemann zeta function and Perron's formula and the Prime Number Theorem for Automorphic L-Functions.

[Yuyang Zhao]

Moreover, it uses Ingham's method to prove the prime number theorem, moves the integration contour from $\Re s > 1$ to $\Re s < 1$ (all very near $\Re s = 1$), and the residue at $1$ contributes to the main term. It doesn't need Hadamard factorization of zeta function.

It only need the properties of zeta function near line $\Re s = 1$, so you can perform analytic continuation only to $\Re s > 0$.

[Alex Kontorovich]

Thanks!! What's written in that description is exactly what we're doing for "MediumPNT", but using more elementary bounds (in fact, now that I look at it, what we're doing matches exactly the argument leading to Titchmarsh (3.6.6)); the argument leading to Titchmarsh's Thm 3.10 uses a Landau-type approach, that is, approximating $f' (s)/f (s)$ near $s_0$ by $\sum_\rho 1/(s-\rho)$ where the sum runs over zeros $\rho$ of $f$ near $s_0$. It is exactly this kind of thing I was hoping to avoid, because I don't know the "right" way to set up such a structure formally. But maybe it's not that bad after all! -- that's exactly what I'm trying to understand about @Meow's approach (but sadly don't have enough Isabelle chops to make sense of the 5000 lines of code...).

[Shuhao Song]

Hello! I'm Shuhao Song, I published a paper on my approach:
https://link.springer.com/article/10.1007/s10817-025-09718-9

[Shuhao Song]

My result essentially corresponds to your unfinished theorem StrongPNT (the strong form of the Prime Number Theorem). However, my version might be even stronger in the sense that I can explicitly compute the constant $c$ in the error term $O(x \exp(-c\sqrt{\log x}))$. I would be delighted to assist your team in completing the formalization of StrongPNT.

[Alex Kontorovich]

That's great, thanks! It would be fantastic if you would like to please formalize the Borel–Carathéodory theorem ("local" Hadamard, Thms 4-6 in your paper) -- and it would be a great contribution to Mathlib, too. Please let me know if that would be of interest to you. It's a rate-limiting step to get to the classical error term. (As you might see in the blueprint, we can already get to the error $O(x\exp(-c(\log x)^{1/10})$ without it, just with completely elementary methods...)

[Shuhao Song]

Alex Kontorovich said:

That's great, thanks! It would be fantastic if you would like to please formalize the Borel–Carathéodory theorem ("local" Hadamard, Thms 4-6 in your paper) -- and it would be a great contribution to Mathlib, too. Please let me know if that would be of interest to you. It's a rate-limiting step to get to the classical error term. (As you might see in the blueprint, we can already get to the error $O(x\exp(-c(\log x)^{1/10})$ without it, just with completely elementary methods...)

OK. I know what you mean.