Explicit estimates: $$M(x)$$, $$\psi(x)$$

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Hi all,

We've discussed before how it would make a lot of sense to formalize explicit bounds in number theory, for a variety of reasons, starting with:

• would you trust a mathematician with adding the bill?
• formalizing explicit results tends to be easier than formalizing theorems with many $O(x)$ and $o(x)$ floating around

I said once or twice that I had something coming up. My paper with A. Chirre on estimates on $M(x) = \sum_{n\leq x} \mu(n)$ is now in the arXiv (https://arxiv.org/abs/2511.14736). We also have a paper on $\psi(x) = \sum_{n\leq x} \Lambda(n)$ coming up very soon.

To some extent estimating $M(x)$ was seen as the harder problem, in that there were no direct analytic explicit bounds on $M(x)$, and the bounds that existed were much weaker than bounds on $\psi(x)-x$, i.e., estimates for the more common form on PNT.

The problem that we solve is that of using a finite spectral information on $1/\zeta(s)$ and $-\zeta'(s)/\zeta(s)$ (or other Dirichlet series with meromorphic continuation) optimally. By "finite spectral information" I mean, at a minimum, a verification that all zeros with imaginary part between 0 and T lie on the line $\Re s = 1/2$; in the case of $M(x)$, we also need information on the residues of $1/\zeta(s)$ (which we can of course compute, since $T$ is finite; all these computations can be done rigorously.)

The approach is a combination of the Tauberian and complex-analytic approach. You can then use the results as the first step of a ladder to construct bounds on $M(x)$ of the form $O(x/\log^k x)$; the main idea of that process was already known - it is related to elementary proofs of PNT in the style of Selberg/Erdős. It will just run much more efficiently now, as what we have is essentially finite explicit formulas.

Tell us if there is interest in producing a formalized version and we can try to help.

Notes:

1. I'd imagine that, at first, the results would assume a verification of RH up to a certain height (and a computation of residues, in the case of $M(x)$) with a 'sorry', or else they can be stated as "if RH is satisifed up to height T...). My understanding is that formalized verifications of RH up to a considerable constant height are very much a realistic hope, but that they most likely be undertaken through systems other than Lean.
2. By the way, very early on in the paper on $M(x)$ (section 3.1), we get yet another proof of $M(x)=o(x)$ (and hence PNT). It is a variant of the Tauberian proof - it just flows very naturally out of our estimates.

[Terence Tao]

I think this would fit very well with the PNT+ project!

Coincidentally, I am also starting to do some large-scale formalization of explicit analytic number theory (having secured some initial funding to get some students to assist). As a proof of concept, I will start with formalizing this argument at https://mathoverflow.net/questions/501066/is-the-least-common-multiple-sequence-textlcm1-2-dots-n-a-subset-of-t?noredirect=1#comment1313839_501066 that uses an explicit PNT of Dusart to establish a certain claim about the least common multiple of the first n numbers for all $n \geq 10^{10}$. (@Bhavik Mehta has already formalized the claim for $n \leq 10^{10}$, so this would close off this problem nicely. I started an initial PR at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/417 containing a blueprint file (obtained from the above comment through AI), and hope to work more on it in the near future.

[Matthew Bolan]

Bhavik actually formalized up to $10^{40}$ (and I made ladders that can take that much higher if need be). I get that the project is only interesting to get some good explicit analytic number theory off the ground though.

[Harald Helfgott]

Are you formalizing Dusart's statement, or are you assuming it?

Dusart statement relies on two results:
a) for moderate x, a bound of the form |\psi(x)-x|\leq \epsilon x based on a finite verification of RH, following Faber and Kadiri's (suboptimal) method;
b) for very large x, a bound of the form psi(x)-x = o(x) in an older paper by Dusart.

For (a), just wait a week or two until our paper on PNT is out. It has the optimal such result of that type. There's not much of a point in formalizing an older, suboptimal result (which is not necessarily simpler or self-contained).

For (b), I agree that formalizing a result of type psi(x)-x = o(x) with good bounds is a priority. I would favor formalizing the strongest result known, namely, Fiori-Kadiri-Swidinsky. Now, it's not self-contained, but the same is true of older results of the form psi(x)-x = o(x) as well - and if anything, this makes the case for formalization stronger: the reliability issue that formalization would solve is more pressing.

Once you have got a result of type psi(x)-x = o(x), and my new results with Chirre, you are all set: you can build a tower of explicit results of type |M(x)|\leq x/\log^k x, for instance, using those two results to get an iteration started.

[Harald Helfgott]

---

Let me stay it very clearly in case it hasn't been already, even at the cost of repeating myself. The entire area of basic estimates regarding primes, $\mu(n)$, etc., as in, say, the first chapters of TME-EMT (https://ramare-olivier.github.io/TME-EMT/Latex/booklet.pdf) rests on two legs:
(a) bounds of the form |psi(x)-x|\leq \epsilon x, $|M(x)|\leq \epsilon x$, etc., relying on finite verifications of RH,
(b) psi(x)-x = o(x), where you want as good an asymptotic rate of decay as realistically possible.

What is new is a provably optimal way of doing (a).
Let me emphasize that it is a priority to formalize (b). In practice, this means formalizing Fiori-Kadiri-Swidinsky. Older results of the same kind are not (as far as I can tell) significantly simpler. Vinogradov-type bounds are stronger asymptotically, but that really kicks in only for extremely large x. I do think they should be formalized, but perhaps a little later.

[Harald Helfgott]

And again to state something that many people know backwards and forwards - why do we need both (a) and (b)?
For psi(x), it is just the very prosaic reason that results of type (a) are much stronger when x is less than 10^1000 or so.
For M(x), you need a result of type $|M(x)|\leq \epsilon x$ and a result of type psi(x)-x = o(x) [sic]; the only practical way known to get explicit results of type $|M(x)| = o(x)$ is based on those two.
And then of course a whole series of results is based on bounds on M(x) rather than psi(x).

[Terence Tao]

Currently I am assuming various explicit PNT estimates such as Dusart's as a black box. My hope is that we will eventually get some semi-automated tooling in which we can take a given application of explicit PNT estimates, plug in whatever explicit estimates we want to use (either the latest ones available, or some older results in the literature, or whatever) and we can automatically see what numerical ranges one can get in the final result (e.g., that a certain statement holds for all $n \geq N_0$ for some explicit $N_0$ that depends on the inputs).

I was thinking of formalizing Rosser-Schoenfeld mainly because of the variety of generally useful estimates present in that paper on various arithmetic functions relating to the primes, again with the hope that one could automatically improve many of these estimates by inserting the latest bounds on say (a) and (b).

I'll take a look at Fiori-Kadiri-Swidinsky, thanks for the pointer!

[Harald Helfgott]

1. I agree that formalizing Rosser-Schoenfeld is a good goal, but (a) formalizing it assuming bounds of the form (a1) |psi(x)-x|\leq \epsilon x and (a2) |psi(x)-x|=o(1) should be rather easy, more of a job for a student (I thought one at Math, Inc. was interested?) (b) there's really no point in formalizing the bounds (a1) and (a2) that Rosser-Schoenfeld use; there are better ways to use even the information on zeros that was available to them.

2. I'd say estimates on sums of mu are at least as useful as much of what you can find in Rosser-Schoenfeld. Here TME-EMT is a good guide as to what gets used in practice. The reason why estimates don't appear Rosser-Schoenfeld is presumably that the explicit estimates on sums of mu available at that point were extremely weak.

3. We'd have to decide what kind of explicit PNT estimates to assume. It is often better to assume not just (a1) but an actual finite explicit-formula expression for psi(x). Then you can get cancellation from the contribution of each x^\rho, for instance.

[Terence Tao]

Thanks, this is helpful. So I guess we can make a distinction between three levels of explicit estimates:

• "primary" explicit estimates such as $|\psi(x)-x| \leq \varepsilon x$, $|M(x)| \leq \varepsilon x$, or $\psi(x) - x = o(x)$, that are proven through zero free regions and numerics (as you say, one may eventually add a few more types of estimates to this category, but these seem like a good place to start).
• "secondary" explicit estimates, such as bounds on $p_{n+1}-p_n$, $\prod_{p \leq x} (1-1/p)$, etc., which are derived from the primary estimates largely through elementary calculations (I am indeed in conversations with Math Inc. about doing this part semi-automatically with current tooling), and the ones that are typically used in applications.
• "tertiary" applications, such as the one I mentioned about demonstrating that $\mathrm{lcm}(1,\dots,n)$ is not highly abundant for large $n$, where each application typically requires its own ad hoc set of arguments.

After looking at Fiori-Kadiri-Swidinsky I think I agree that for the primary estimates it makes sense to formalize just the most recent results as the increase in complexity is not so great. Any tertiary result can be formalized independently assuming whatever secondary inputs are available (and one can try to set the formalization up with all explicit constants replaced by parameters, with the final theorem being something to the effect of "if one can select parameters obeying this finite list of constraints, and the requisite secondary estimates with the specified parameters are true, then the desired conclusion holds at scales indicated by the parameters").

To get from the primary estimates to the secondary estimates I can imagine that there could be a variety of methods of varying efficiency, with various papers such as Rosser-Schoenfeld, Dusart, Buthe, etc. containing various useful lemmas to aid in the transfer from the former to the latter. Hopefully these lemmas can be abstracted away from specific numerical choices of parameters (in the spirit of the ANTEDB) and then combined together by various other tools (in the ANTEDB we used hand-written python code to optimize the combinations, but nowadays one could imagine an AI-assisted, Lean-formalized route instead).

Given this, I think I might focus for now on the primary->secondary and secondary->tertiary type of implications, leaving the primary estimates as black boxes; but if for instance you want to initiate a project to formalize some of your primary estimate results, that would mesh well with this.

In the immediate term I have a number of other things to attend to, but I will try to at least make a basic blueprint framework for this structure soon.

[Harald Helfgott]

It's just as well for me if you work on the primary->secondary and secondary->tertiary stages, since I don't find them particularly interested :).

a) I don't think it would necessarily make most sense for me to be the only person in charge of formalizing my primary estimate results; I haven't produced a blueprint before - and the person who writes a paper is rarely the best one to explain it. What would make sense would be for me to team with at least one volunteer who has written blueprints before.
b) From my perspective, formalizing Fiori-Kadiri-Swidinsky is a priority, but that's purely subjective: I already know my own result backwards and forwards. FKS, like other modern zero-free-region-based results, is a bit of a "fox" proof rather than a 'hedgehog" proof, and so a check would be particularly valuable.

[Harald Helfgott]

It would best to have on board as many people from TME-EMT on board. Most of them have not engaged in proof formalization even peripherically, and I know there's a steep learning curve, so it would be necessary to have precise instructions on "what is a blueprint?" as well as a detailed map of the analytic results that are and aren't available. I should say that non-explicit limiting processes (which apparently can be a pain to formalize, according to a different thread) are sometimes used in proving explicit results, particularly when they matters more elegant.

Another group of folks that have expressed interest are those in Math, Inc. (mostly Jared Duker Lichtman and some very junior people).

[Harald Helfgott]

Just a heads-up that Andrés Chirre and I will finally post our paper on $\psi(x)-x$ to the arxiv later this week. (We posted the companion paper on M(x) a month ago: https://arxiv.org/abs/2511.14736)

[Harald Helfgott]

Oh, and I just learned that there was a thesis this year with new zero-free regions: https://doi.org/10.26190/unsworks/31825 . It doesn't seem overly complicated - it seems worthwhile to look into formalizing it.

[Harald Helfgott]

Sorry, wrong conversation. Let me say the same under 'Explicit estimates...'

[Harald Helfgott]

Oh, and I just learned that there was a thesis this year with new zero-free regions: https://doi.org/10.26190/unsworks/31825 . It doesn't seem overly complicated - it seems worthwhile to look into formalizing it.

[Notification Bot]

2 messages were moved here from #PrimeNumberTheorem+ > Wiener-Ikehara source by Ruben Van de Velde.

[Harald Helfgott]

As to when you would use each of those two results, and what had been done in the literature - we've done our best to explain that in sections 1.3 and 10.1 of the paper.

[Harald Helfgott]

Here it is: https://arxiv.org/abs/2512.15709