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

[Terence Tao]

A brief update on what I've been doing at my end.

I have managed to formalize the statements of the second paper of Fiori, Kadiri, and Swidinsky (FKS2) into the blueprint, see here. Roughly speaking, this paper shows that any explicit prime number theorems with classical error term controlling $\psi(x)$ implies similarly explicit prime number theorems with classical error term controlling $\theta(x)$ or $\pi(x)$. As one would imagine from explicit analysis, the computations are messy, but reasonably self-contained, and should be relatively straightforward to formalize; once some project tooling is in place I may start launching tasks to do that (and also the separate LCM tertiary project which is significantly simpler).

Significantly more challenging is the first paper of Fiori, Kadiri, And Swidinsky (FKS), which establishes an explicit prime number theorem for $\psi(x)$. What I am finding is that this paper is highly non-self-contained. For instance, it relies on a complicated explicit zero density theorem of Kadiri, Lumley, and Ng (KLN), the main statement of which already requires the introduction of several dozen auxiliary quantities to even state (you can get a hint of this by browsing through this Lean file. This paper KLN in turn relies on previous foundational work, for instance by Rosser and Schoenfeld, on explicit Riemann-von Mangoldt theorems and the like.

Another import to FKS concerns explicit Perron formulae. Here I encounter the following disturbing text in Remark 3.3:

We note that the above work [5] of Cully-Hugill and Johnston is currently being peer reviewed, whereas the earlier articles [8] and [31] have errors. While these errors can be corrected, doing so may not recover the claimed results. Dudek’s result was used in Platt and Trudgian’s [30] and represented a non-negligible part of the error term for ψ(x) there. However, in our present application we shall eventually take T large enough that this term becomes negligible. As the choice of version we use would ultimately not impact our results, we have decided to use the worse bound published while including the more stringent hypothesis of [5, Theorem 1.2]. The bound of Proposition 3.4 is Dudek’s bound as stated in [8, Thm 1.3] and is worse by a factor of (logx) than Cully-Hugill and Johnston’s.

(The context here is that they are citing three forms of the explicit Perron formula in the literature, but ending up using the one with the worst bounds because the correctness of the other two versions are in doubt.)

A third input to FKS is, unsurprisingly, an explicit classical zero-free region, which involves a constant $R$ which one would like to be as small as possible. In the paper they use the value $R = 5.5666305$ which comes from a 2015 paper of Mossighoff and Trudgian; in Remark 1.3 they mention that the improved value $R=5.558691$ was recently obtained in 2022 by Missighoff, Trudgian, and Yang, but FKS did not updated their tables and estimates in this paper to incorporate this new value. (This would be one of the most obvious early applications of formalizing FKS.)

All in all, this is not the most "fun" sequence of papers to work through (through no fault of the authors, I should stress, who have tried their best to be careful and organized through all of this), but by the same token I feel that this is precisely the type of unglamorous mathematical infrastructure that (a) needs to be formalized, and (b) should have the computations offloaded from humans to automated tools as much as possible.

Hopefully one of the outcomes of this project will be to create a kind of "Excel spreadsheet" for these sorts of results in which one can explicitly input various numerical parameters to inputs of the form indicated above and see in real time what the (Lean-verified) outputs are, in particular being able to swap in and out results that have not yet been formalized and are under suspicion for one reason or another.

I'll continue to formalize the statements of FKS, but after that I think I will be focusing on getting FKS2 (and LCM) to a point where something like this "spreadsheet" becomes feasible. This will probably occupy most of my bandwidth for this project; if there are others who are interested in taking the lead on formalizing other explicit papers, please let me know and we can coordinate, but I will probably not be able to play a leading role for any other papers until the FKS papers are in better shape.

[Harald Helfgott]

Thank you for this, Terry.

I already had a notion of how the sausage was made, so to speak. That is precisely why formalizing the first paper of FKS (say) is a priority. The importance of having an explicit PNT should be evident, and obviously its reliability is key; that sort of result gets used everywhere. The reality is that, as you say, it is the kind of result that depends on many other results, some of them unreliable. This is not a one-time occurrence - you will find other cases similar to the one you have highlighted above.

What I have been able to do on my end is simply to see what I can prove without using PNT, zero-free regions, etc. (answer: plenty), but it would obviously be preferable to have a fully reliable explicit PNT - and formalization will take care of that issue in a convincing way.

Of course this also means that the task is non-trivial and may be unpleasant.

I agree that it would be ideal to structure things in such a way that, say, an improvement to the classical free region (as in Yang's thesis, say) would automatically give an improvement on the error term.

[Harald Helfgott]

On my end: what I have done with Chirre is independent of any explicit PNT results. There are plenty of interesting consequences one can get from that when one puts it together with explicit PNT (for instance, one would get good explicit bounds of type M(x) = O(x/\log x), M(x) = O(x/log^2 x)) but obviously I'm concerned about the solidity of the ground on which we would be standing. From this perspective, formalization is a must.