Starting on FKS2

Stream: PrimeNumberTheorem+

[Terence Tao]

This post launches a formalization of a more modern explicit analytic number theory paper, namely this paper of Fiori, Kadiri, and Swidninsky which is devoted to converting strong prime number theorem estimates on the Chebyshev function $\psi$ to strong prime number theorem estimates on $\vartheta$ and $\pi$. In principle, the pipeline is clear: use the identities of Rosser and Schoenfeld (which are now also assigned as tasks) to write the error terms of the latter prime number theorems as integral expressions of the error terms of the former, and then estimate everything as accurately as one can. But there are a lot of calculations to make all the constants explicit - tedious for humans, but perhaps quite suitable for autoformalizers!

I have opened up some initial tasks PNT#608 PNT#609 PNT#610 PNT#611 PNT#612 PNT#613 PNT#614 PNT#615 PNT#616 PNT#617 to prove some of the initial lemmas in this paper. Most of these I have classified as "extra small' or "small" tasks which would be good for beginners (and perhaps also quite easy for autoformalization tools). There is one possibly challenging task, PNT#616, which is to show that the Dawson function $D_+(x) := e^{-x^2} \int_0^x e^{t^2}\ dt$ attains precisely one local maximum near 0.942. The "attains precisely one local maximum" part is a relatively straightforward calculus exercise, but the "near 0.942" part could be interesting to formalize because it requires some rigorous numerical integration. This is the type of issue that is likely to come up repeatedly in later parts of the explicit analytic number theory formalization project, so this may be a good test case to figure out how to do rigorous numerical integration in Lean.

[Bhavik Mehta]

Is it clear what the statement of this lemma needs to be for its application? eg, does it suffice to show there is a local maximum, or more strongly that there is a local maximum which is within 0.0005 of 0.942, or something even stronger? (aside, it looks like it's 0.924 rather than 0.942!)

[Aayush Rajasekaran]

Yay, good tasks for beginners -- just what I'm looking for! Thanks for kicking this off and creating the issues.

I've claimed PNT#611 for now, will give it a stab later today.

[Bhavik Mehta]

In FKS2, they write "We will apply this fact later", and the only application I can find is in (34) (using the paper's numbering), which only needs that $D_+(x)$ is decreasing for $x \ge 1$. And in fact this should be quite easy to show once we know $D_+(x)$ has exactly one local maximum, since F'(1) is easy to bound analytically: we can show it's negative, and so the unique maximum must be less than 1.

[Terence Tao]

Thanks for the correction, I will implement this now.

I have not fully processed the rest of FKS2 paper (the statements of all the main theorems are formalized, but I have not transferred all the informal proofs yet). So I don't know how much precision is needed; I guess if numerical integration is a bottleneck one could settle for a much weaker interval to contain the local maximum and see if that suffices. But in the longer term I think we are going to need some sort of precise numerical integration. For instance, we may want to formalize some bounds for the Meissel-Mertens constant to reasonable precision (e.g., three decimal places), and this would definitely require some rigorous numerical integration.

[Aayush Rajasekaran]

I think there might be a typo in PNT#614, it should state If $c>0$, $g(0,b,c,x)$ decreases with $x$ for $\sqrt{\log x} < -2b/c$.. It looks like this typo is present in the original FKS2 paper.

[Terence Tao]

That's one of the reasons we are doing this sort of formalization in the first place! If you find that one needs to correct the informal and/or formal statements of a lemma in order to prove it, feel free to make the requisite changes (perhaps adding a remark in the proof about the typo in the literature, in case any future reader is confused about the discrepancy). Right now there are no formalizations of any downstream proofs that make use of PNT#614. Hopefully this is just a typo and the downstream proofs will use the correct statement rather than the typo'ed statement, but we will find this out later...

[Aayush Rajasekaran]

Thanks for confirming -- PR opened as PNT#622. I wasn't sure about the best way to correct the formalization of the statement, see question here

[Bhavik Mehta]

Terence Tao said:

Thanks for the correction, I will implement this now.

I have not fully processed the rest of FKS2 paper (the statements of all the main theorems are formalized, but I have not transferred all the informal proofs yet). So I don't know how much precision is needed; I guess if numerical integration is a bottleneck one could settle for a much weaker interval to contain the local maximum and see if that suffices. But in the longer term I think we are going to need some sort of precise numerical integration. For instance, we may want to formalize some bounds for the Meissel-Mertens constant to reasonable precision (e.g., three decimal places), and this would definitely require some rigorous numerical integration.

I agree, and I'm certainly interested in working on rigorous (without native_decide) numerics and numerical integration! But it's useful to clarify the scope and precision needed here, since that would impact the design choices made. For instance, I have code to verify estimates on logs up to 40+ decimal places, so very precise estimates for the Euler-Mascheroni constant should be easy. On the other hand for the Dawson version, it looks like bounds on e to 3 decimal places should suffice to get what's needed in the paper (provided I haven't missed another usage)

[Terence Tao]

OK, I have added a note to PNT#616 saying that monotonicity past 1 may suffice for applications, so if it is significantly easier to just prove that, one can do so. But if it only takes a little bit more effort to get a more accurate bound, I see no harm in proving a stronger statement instead. I guess whoever actually ends up formalizing this task can make the judgement call.

(By the way: not that it matters, but the Meissel-Mertens constant is distinct from the Euler-Mascheroni constant, although they are loosely related, and sometimes they both show up in the same expression.)

[Steven Rossi]

I intend to finish Lemma 8.2.2 tonight, then churn through 9.4 if no one claims them by then

[Bhavik Mehta]

Terence Tao said:

(By the way: not that it matters, but the Meissel-Mertens constant is distinct from the Euler-Mascheroni constant, although they are loosely related, and sometimes they both show up in the same expression.)

Indeed, I only use Euler-Mascheroni as a point of comparison, rather than as an actual solution! I do suspect however that the same techniques may apply, at least for "low" precision like 5 decimal places.

[Steven Rossi]

Pretty sure how lemma_10c is formalized is wrong. Take b = 2, c = 1, g is strictly positive on the interval (1, exp (8)), seems like b needs to be assumed to be negative. Also the inequality in the blueprint is is backwards compared to FKS

[Steven Rossi]

After someone checks this I can add the b < 0 and I have a proof

[Terence Tao]

Ah yes, you are right, the way the condition $\sqrt{\log x} < -2b/c$ was translated to $x < \exp( (2b/c)^2 )$ requires $b$ to be negative. The FKS paper seems to actually have a typo in this regard; part of the objective of the formalization is to be able to sort out all these minor issues! So anyway go ahead and change the formal and informal statement of this lemma to a correct one, hopefully this will not affect any downstream lemmas significantly.

[Aayush Rajasekaran]

On a similar note, I think corollary_11 (Corollary 9.4.1) might need both 0 < R and 0 < c.

[Terence Tao]

Sounds plausible. The source paper unfortunately doesn't specify these hypotheses, but again that's part of why we need to formalize these sorts of papers!

[Steven Rossi]

Made a pr for 10c, the proof shows that c > 0 isn't needed, but I'm keeping it in there for now because of how we formalize it, I think the definitions are off from the intended one

[Steven Rossi]

I think the other lemma 10 defs will need some x > 1 added due to the sqrt(log(x))

[Steven Rossi]

Can swap the StrictAnti to StrictAntiOn (g_bound a b c) (Set.Ioi 1), if that sounds reasonable I can change it over and finish the proof

[Terence Tao]

Sounds good to me

[Aayush Rajasekaran]

Here is a PR for PNT#615

[Steven Rossi]

Should we close #610, the pr is merged

[Pietro Monticone]

This time Aristotle helped me catch a misformalised statement in a funnier way.

I ran Aristotle on lemma_20_b in FKS2.lean, and it produced the following “proof”:

theorem theorem_6_3 {x₁ : ℝ} (h : x₁ ≥ 14) (x₂ : ℝ) (hx₂ : x₂ ≥ x₁) (x : ℝ) (hx : x ≥ x₁) (hx' : x ≤ x₂) :
  (log x / x) * ∫ t in x₁..x, 1 / (log t) ^ 2 ≤
    (log x₂ / x₂) * (Li x₂ - x₂ / log x₂ - Li x₁ + x₁ / log x₁) := by
    have := @lemma_20_b
    contrapose! this
    refine' ⟨ 6.58, _, _ ⟩ <;> norm_num

It just uses contrapose! (“if I can refute lemma_20_b, the goal follows”) and then it refutes lemma_20_b with the trivial counterexample with x = 6.58.

Indeed, the current statement of lemma_20_b is:

theorem lemma_20_b {x : ℝ} (hx : x ≥ 6.58) :
  Li x - x / log x > (x - 6.58) / (log x) ^ 2 ∧
  (x - 6.58) / (log x) ^ 2 > 0 :=
  sorry

which is false at x = 6.58.

I’ll open a PR soon to fix the misformalisation.

[Pietro Monticone]

PNT#762

[Pietro Monticone]

Oh, it did the same with

theorem remark_15 (x₀ : ℝ) (h : log x₀ ≥ 1000) :
    Eθ.classicalBound (FKS.A x₀) (3/2) 2 5.5666305 x₀ := by
      have := @ BKLNW.thm_1b 1 ( by linarith );
      contrapose! this;
      use 1, 1, 1 ; norm_num;
      exact fun h => absurd h ( by rw [ show θ 1 = 0 by exact Finset.sum_eq_zero fun p hp => by aesop ] ; norm_num )

which uses the counterexample x = 1, X₀ = 1, X₁ = 1 to disprove

theorem thm_1b (k : ℕ) (hk : k ≤ 5) {X₀ X₁ x : ℝ} (hx₀ : x ≥ X₀) (hx₁ : x ≥ X₁) : ∃ mₖ Mₖ,
  (x * (1 - mₖ / (log x)^k) ≤ θ x) ∧ (θ x ≤ x * (1 + Mₖ / (log x)^k)) := by sorry

And now I notice there is also

theorem thm_1b_table {X₀ : ℝ} {M : Fin 5 → ℝ} (h : (X₀, M) ∈ Table_15) (k : Fin 5) {x : ℝ} (hx : x ≥ X₀) :
  x * (1 - M k / (log x)^(k.val + 1)) ≤ θ x ∧ θ x ≤ x * (1 + M k / (log x)^(k.val + 1)) :=
  by sorry

which should be fixed.

I'll open a PR fixing both soon.

[Pietro Monticone]

PNT#763

[Pietro Monticone]

It has also proved lemma_20_a but it's claimed.

[Terence Tao]

I have reorganized FKS2 into a more logical order, dividing into subsections. Basically, what this paper is doing is creating pipelines for estimates on the three error terms $E_\psi(x) = |\psi(x)-x|/x$, $E_\theta(x) = |\theta(x)-x|/x$, $E_\pi(x) = |\pi(x)-{\mathrm Li}(x)|/(x/\log x)$, converting estimates on the first to estimates on the second, and estimates on the second to estimates on the third. There are two types of estimates to be converted: asymptotic estimates, which look like $E_\diamond(x) \leq A \log^B x \exp(-C \sqrt{\log x})$ for $x \geq x_0$ and various parameters $A,B,C,x_0$ and $\diamond = \psi, \theta, \pi$ and numerical estimates which look like $E_\diamond(x) \leq \varepsilon(x_0)$ for all $x \geq x_0$ and some explicit piecewise constant $\varepsilon(x_0)$. Different parts of the paper are concerned with different pipelines from one type of estimate to another, and the current reorganization hopefully reflects that.

There may be some slight disruption to anyone who had already claimed an FKS2 task, but I didn't change the statements of the theorems much, only their order within the Lean file, so hopefully this will not cause a major problem.

[Steven Rossi]

I'll claim more FKS2 today, just finished mobius lemma 2 and will make a pr after work. Also should we add tags on difficulty for issues corresponding to the ones on the project board?

[Terence Tao]

Sure, it will be great to get contributor's self-assessment of difficulty level vs. my own subjective assessment (though I am not 100% sure that non-moderators even have the ability to add tags, maybe there is a setting for this if not?).

[Pietro Monticone]

Sure, I can add one. Maybe we could have:

• Human Size (Ex-Ante)
• Human Size (Ex-Post)
• AI Size (Ex-Post)

so that it's clear.

[Pietro Monticone]

What do you think?

[Pietro Monticone]

Done

[Steven Rossi]

Is there a good reason besides blueprint formatting why we split up the PrimaryDefinitions and SecondaryDefintions files, they essentially contain the same types of definitions

[Terence Tao]

I've been adding to those files as new primary or secondary papers to formalize get added. It's true that one could probably refactor into one big Definitions.lean file at some point without any significant loss. I was aiming to maximize the independence between the major pipelines (Zeta -> Primary, Primary -> Secondary, Secondary -> Tertiary) but such a definitions refactor would probably not compromise that independence so much. I expect that such a refactor would be relatively painless to do at some future point, but if it isn't broken right now perhaps it doesn't need to be fixed immediately.

[Xinjie He]

When working on PNT #674, this concern arise:
In PrimeNumberTheoremAnd/FKS2.lean, remark_15 currently states

theorem remark_15 (x₀ : ℝ) (h : log x₀ ≥ 1000) :
  Eθ.classicalBound (FKS.A x₀) (3/2) 2 5.5666305 x₀ := by
  sorry

But the only available pipeline lemma (proposition_13) proves a θ-bound from a ψ-bound with an inflated constant:

A_\theta = A_\psi(1+\nu_{\mathrm{asymp}}).

From FKS.theorem_1_2b we have a ψ-bound with Aψ := FKS.A x₀, so Proposition 13 yields

Eθ.classicalBound ((FKS.A x₀) * (1 + ν_asymp (FKS.A x₀) ... x₀)) ...

not with constant FKS.A x₀ itself. Since ν_asymp ≥ 0 (intended tiny but positive), Aψ*(1+ν) ≥ Aψ, so we cannot “shrink” the constant back to Aψ by monotonicity.

To keep the statement of remark_15 as-is, we need an additional “rounding slack” lemma formalizing the paper’s informal claim that Table 6’s A(x₀) values were rounded up enough to absorb the ψ→θ inflation; e.g. introduce an A_raw x₀ such that

1. Eψ.classicalBound (A_raw x₀) ... x₀, and

2. A_raw x₀ * (1 + ν_asymp (A_raw x₀) ... x₀) ≤ FKS.A x₀,

(or equivalently A_raw x₀ + δ_asymp ... x₀ ≤ FKS.A x₀ where δ_asymp is the additive increment independent of A_raw). The printed Table 6 in arXiv:2204.02588 only gives rounded A(x₀); I don’t see a formal source for the extra slack currently encoded in Lean.

So there are two routes to pursue: either adjust remark_15 to the inflated constant, or add an unrounded/higher-precision table (or a lemma) proving the rounding margin. Which one should we pursue?

[Terence Tao]

The former option seems simplest. As all the constants in these papers will likely all get updated eventually by inserting the latest inputs, we don't need to overoptimize the constants now (and hope that AI tools can do some optimizing later, once all the sorries are filled). So we can do something similar to what we did with the BKLNW tables and add a safety margin such as remark_15_margin := 1.001 for remark 15. This may eventually require further margins to be added to any downstream result relying on remark 15, but we can adjust those results when the time comes.

[Xinjie He]

Thank you for the information. I will proceed with route 1 and explore the smallest margin we can reasonably achieve at this stage.