Update on tertiary estimate projects

Stream: PrimeNumberTheorem+

[Terence Tao]

A small update on the "Explicit analytic number theory project" I have soft-launched within this PNT+ project. I have not yet made a full launch of this project, as some of the infrastructure (e.g., the issues-based project management system) is not yet in place; but some components of the project are already active and being used as test cases for the larger project.

The idea of the project is to formalize and integrate several types of explicit analytic number theory estimates, which one can roughly classify into three categories:

1. "Primary estimates" that estimate the Chebyshev function $\psi$ or the Riemann zeta function $\zeta$, with explicit constants.
2. "Primary -> Secondary estimates" that convert the type of primary estimates in the first category to estimates on other basic number-theoretic functions of interest, such as the prime counting function $\pi(x)$, the error term in Mertens' type theorems, etc.
3. "Secondary -> Tertiary estimates" that use secondary estimates to solve various other problems in analytic number theory, again with explicit constants.

Here I will report on the third category, where I have written up blueprints for two results of this type:
3a. An argument showing that $L_n = LCM(1,\dots,n)$ is not a highly abundant number for all sufficiently large $n$ (specifically, $n > 89693^2$). The argument relies on a secondary estimate of Dusart regarding the existence of primes in short intervals, which is stated in Lean right now, but for which no blueprint exists to describe its proof.
3b. An argument solving Erdos problem 392, which asks to factor $n!$ into at least $n/2 - n/2\log n + o(n / \log n)$ factors that all do not exceed $n^2$. Technically this argument only needs the qualitative prime number theorem due to the $o()$ error, but in principle the formalization could uncover an explicit error bound (contingent on importing known effective secondary estimates from e.g., Rosser-Schoenfeld into the Lean codebase).

Thanks to the quiet work of many contributors including @Pietro Monticone and my mentees here at UCLA (Xinjie He and Hjunsik Chae), a fair chunk of the subtasks needed to prove 3a and 3b have already been completed. But there is definitely room for further volunteers to help finish the tasks here. Here are some "outstanding tasks" for 3a that could be claimed here (before we move over to an issues based system):

3a.1. Lemma 134 (factorization of $L_n$) Assuming the existence of certain parameters obeying some conditions (as formalized in the Criterion structure), the LCM $L_n$ can be factored into three primes $q_1,q_2,q_3$ and a remainder $L'$. This should be straightforward to formalize. (Formalized by @Snir Broshi and @Xinjie He )
3a.2. Lemma 135 (normalized divisor sum $L_n$) Relates the divisor sum of $L_n$ to the divisor sum on $L'$. This should follow from the multiplicativity properties of the divisor sum. (Formalized by @Pietro Monticone )
3a.3. Lemma 137 (basic properties of $M$) Constructs a competitor $M$ to $L_n$ and proves that it is slightly smaller than $L_n$. This should be elementary manipulation of inequalities. (Formalized by @Pietro Monticone )
3a.4. Lemma 138 (a sufficient inequality) By comparing $M$ with $L_n$, gives a sufficient condition for $L_n$ to not be highly abundant. This is largely just substituting in definitions and using the previous Lemma. (Formalized by @Pietro Monticone )
3a.5. Lemma 139 (reduction to a lower bound for $\sigma(M)/M$) By combining Lemma 138 with Lemma 135 one can reduce to a more tractable sufficient condition to not be highly abundant. (Formalized by @Pietro Monticone )
3a.6. Lemma 140 (Lower bound for $\sigma(M)/M$) Uses multiplicativity to verify the condition produced in Lemma 139, provided that the primes $p_1,p_2,p_3,q_1,q_2,q_3$ obey a certain explicit inequality. (Claimed by @Yan Yablonovskiy 🇺🇦 )
3a.7 Lemma 141 (choice of medium primes) Uses the explicit prime number theorem of Dusart to locate primes $p_1,p_2,p_3$ with good estimates. (Formalized by @Pietro Monticone )
3a.8 Lemma 142 (choice of large primes) Uses the explicit prime number theorem of Dusart to locate primes $q_1,q_2,q_3$ with good estimates. (Claimed by @Aaron Hill )
3.a.9 Lemma 143 (Bounds for the $q_i$-product) Bounds one of the terms needed in the explicit inequality. (Formalized by @Alex Kontorovich )
3.a.10 Lemma 144 (Bounds for the $p_i$-product) Bounds one of the terms needed in the explicit inequality.
3.a.11 Lemma 145 (Lower bound for the product ratio $p_i/q_i$) Bounds yet another term needed in the explicit inequality.
3.a.12 Lemma 146 (Uniform bounds for large $n$) Bounds some of the terms involving $n$ (Formalized by @Pietro Monticone )
3.a.13 Lemma 147 (Polynomial approximation of the inequality) Bounds some expressions by polynomials in the quantity $\varepsilon = 1/n$ (Formalized by @Pietro Monticone )
3.a.14 Proposition 8 (Verification of criterion for large $n$) Verifies the criterion for $n$ large enough.

If anyone wants to contribute to the project by claiming one or more of these tasks, please be my guest!

One could make a similar list for 3b, but given that we may switch over soon to a different system, I'll be happy to focus on 3a for now. Also if there are other suggestions for similar results that could fit into this network of estimate, I'd be happy to take them into consideration; it seems that with modern AI tools we can formalize these results at a significantly faster rate than with previous projects of this type.

Incidentally it will probably be a good idea going forward to change the lemma numbering system to make it more stable (currently if we add lemmas in a previous section it will update all the section numbers in later sections). According to an AI, this is just a matter of adding \newtheorem{lemma}{Lemma}[section] and the like to the preamble, but this will also affect all the other sections of the blueprint. Are there any objections to implementing such a change?

[Snir Broshi]

Hello :wave: I want to try to contribute, number theory is a bit outside my comfort zone but I'll give it a shot.
This is 3a.1 (lemma 134):

theorem Criterion.ln_eq (c : Criterion) : L c.n = c.q 0 * c.q 1 * c.q 2 * c.L' := by
  rw [L', ← Fin.prod_univ_three, Nat.mul_div_cancel' <| Fintype.prod_dvd_of_isRelPrime ?_ ?_]
  · refine fun i j h ↦ Nat.coprime_iff_isRelPrime.mp ?_
    exact Nat.coprime_primes (c.hq i) (c.hq j) |>.mpr <| c.hq_mono.injective.ne h
  refine fun i ↦ Finset.dvd_lcm <| Finset.mem_Icc.mpr ⟨c.hq i |>.one_le, le_trans ?_ c.h_ord_3.le⟩
  exact c.hq_mono.monotone <| Fin.le_last i

Harder than expected but doable. Is there a place to claim, or should I PR?
General question: How common is it to add helper lemmas to upstream to Mathlib? I see the Mathlib/NumberTheory folder is pretty empty, is that because a lot was upstreamed or because the project prefers to prove things inline when possible? (I'm specifically asking about your project rather than the PNT+ project)

[Ruben Van de Velde]

Please add mathlib-ready lemmas where you can (and bonus points for upstreaming them immediately)

[Terence Tao]

That was fast! Please feel free to PR your proof.

[Pietro Monticone]

I can claim Criterion.q_not_dvd_L' if it's ok.

[Snir Broshi]

I think I'm close to finishing it, can you do a different one please?

[Pietro Monticone]

Oh, sure! No problem.

[Pietro Monticone]

Ok, so I would claim 3a.3. Lemma 137 (basic properties of $M$).

[Snir Broshi]

I got stuck on Criterion.q_not_dvd_L'; reduced it to:

@[simp]
theorem prime_pow_dvd_ln_iff {p n : ℕ} (hp : p.Prime) (hn : n ≠ 0) (k : ℕ) :
    p ^ k ∣ L n ↔ p ^ k ≤ n := by
  sorry

which might follow from:

theorem foo {n : ℕ} : L n = ∏ pk ≤ n with IsPrimePow pk, pk.minFac := by
  sorry

(also related to Real.log (L n) = ∑ k ≤ n, vonMangoldt k)
Do we have any of these, or does anyone know how to prove them? I'm not sure what to induct on

[Pietro Monticone]

Opened PNT#470 solving 3a.3. Lemma 137 (basic properties of $M$) and golfing prod_p_le_prod_q.

[Terence Tao]

Perhaps one could first extend docs#Nat.factorization_lcm to docs#Finset.lcm? Something like

theorem Nat.factorization_finset_lcm {β:Type*} (s : Finset β) (f : β → ℕ) (p: ℕ)
  : (s.lcm f).factorization p = iSup (fun b ↦ ((f b).factorization p))
  := by sorry

(perhaps there is a better way to spell this, also one may possibly need Nonempty s). Presumably this can be deduced from docs#Nat.factorization_lcm by induction (and then perhaps it would be suitable for moving into Mathlib?).

[Pietro Monticone]

I would claim 3a.4. Lemma 138 (a sufficient inequality)

[Pietro Monticone]

Opened PNT#471 solving 3a.4. Lemma 138 (a sufficient inequality)

[Pietro Monticone]

I proved 3a.5. Lemma 139 (reduction to a lower bound for $\sigma(M)/M$) too because it's almost immediate from lemma 138.

[Pietro Monticone]

PNT#472

[Terence Tao]

I may possibly have sliced up the proof into pieces that are so small as to be trivial, but I guess that's a good thing!

[Pietro Monticone]

Maybe not really trivial since they are full of annoying coercions and forced type annotations. The good news is that they are very similar: once you have solved those issues for one, much of the work carries over to the others it seems...

[Pietro Monticone]

I can claim lemma 135 but it requires some refactoring.

[Pietro Monticone]

PNT#473

[Yan Yablonovskiy 🇺🇦]

May i claim Lemma 140 (Lower bound for $\sigma(M)/M$) ? It doesn't seem too bad given 138 and 139.

[Pietro Monticone]

I would claim lemma 141 then

[Terence Tao]

140 is used to verify the hypothesis of 139, but 139 is not used in the proof of 140, which is elementary multiplicative number theory. It might be slightly challenging if you are not already familiar with the multiplicative number theory portions of Mathlib, but I think it should be doable

[Terence Tao]

There are some minor typos in the blueprint proof of Lemma 140, fixing them now.

[Aaron Hill]

I'd like to claim lemma 142

[Pietro Monticone]

Are we sure prod_epsilon_ge holds with 3.37?

[Pietro Monticone]

I can formalise it (very inefficiently and by increasing maxHearthbeats) with 3.36. Let me check with Aristotle...

[Pietro Monticone]

It was immediately negated:

theorem prod_epsilon_ge (ε : ℝ) (hε : 0 ≤ ε ∧ ε ≤ 1 / (89693 ^ 2 : ℝ)) :
    (∏ i : Fin 3, (1 + ε / (1.000675 : ℝ) ^ (2 * ((i : ℕ) + 1 : ℝ)))) *
        (1 + (3 : ℝ) / 8 * ε) * (1 - 4 * (1.000675 : ℝ) ^ 12 / 89693 * ε) ≥
      1 + 3.37 * ε - 0.01 * ε ^ 2 := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- Let's choose $\epsilon = \frac{1}{89693^2}$.
  use 1 / 89693^2;
  -- Simplify the expression by factoring out common terms.
  norm_num [Fin.prod_univ_succ, Fin.prod_univ_zero] at *

[Eric Vergo]

I'd like to claim lemma 147

[Pietro Monticone]

@Eric Vergo is it prod_epsilon_ge?

[Pietro Monticone]

Oh, sorry. I didn't claim it before...

[Eric Vergo]

yes, it looked doable but it looks like it wasn't!

[Terence Tao]

Ah, you are right, those little factors of 1.000675 actually pile up a little bit. But we have room to revise the constant 3.37 downward, so long as Lemma 148 still holds, so maybe if you push it down a little further, it may be easier to prove?

[Pietro Monticone]

Ok, let me see...

[Terence Tao]

This is precisely the sort of arithmetic calculation I am more than happy to offload to Lean / Aristotle!

[Terence Tao]

Alternatively one could simply skip 147 and prove a version of 148 using the more complicated expressions in the left-hand side of 147

[Eric Vergo]

That was my plan (Claude code), it looked just on the boundary of what I thought it could do.

[Terence Tao]

I realized that I was approaching this part of a proof like a human, simplifying the expressions before verifying them numerically. But an AI doesn't really care if the expressions look simple, they can deal with messy expressions directly.

[Terence Tao]

In any case feel free to refactor this portion of the proof (e.g., by merging Lemma 147 and 148) if it is more natural for Lean / AI tools to work with the expressions directly.

[Pietro Monticone]

Opened PNT#477 solving 3.a.13 Lemma 147 (Polynomial approximation of the inequality)

[Pietro Monticone]

Opened PNT#478 solving 3a.7 Lemma 141 (choice of medium primes)

[Harald Helfgott]

Hi all -

For context, let me quote from the bibliography (or list of proposed tasks) given in https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/ :

• [Buthe] J. Büthe, Estimating 𝜋(𝑥) and related functions under partial RH assumptions, Math. Comp., 85(301), 2483–2498, Jan. 2016.
• [Buthe2] J. Büthe, An analytic method for bounding 𝜋(𝑥). Math. Comp., 87 (312), 1991–2009.

I don't want to come across as tooting my own horn, but, while Büthe's results were remarkable at the time, and remained the best available for ten years, the main result of [Buthe] has now been superseded.

Andrés Chirre and I recently posted a preprint (https://arxiv.org/abs/2512.15709) giving a stronger result of the same general form, namely, $|\psi(x)-x| \le \varepsilon x.$ To be precise, we give our bound in the form

$$|\psi(x)-x|\leq \varepsilon(T) x + C(T) \sqrt{x},$$

where $\varepsilon(T)$ and $C(T)$ are explicit functions of the height $T$ up to which RH has been verified.

In fact, we show one can take $\varepsilon(T) = \frac{\pi}{T-\pi/3-1}$, which is essentially optimal.

(To be persnickety: it is $\frac{\pi}{T-\pi/3}$ that would be optimal, and we do reach that asymptotically; that $-1$ in the denominator of $\frac{\pi}{T-\pi/3-1}$ is just a convenient carpet under which to hide some $o(x)$ error terms that are extremely tiny -- smaller than $\frac{x}{T^2}$.)

In addition: compared to Büthe's paper and some previous work, the argument is simpler in several respects. In particular, the special function used by Büthe (viz., the Logan function) disappears; the optimal weight turns out to be a simple hyperbolic trigonometric function. If our paper is somewhat long, it is precisely because we have made an effort to keep it self-contained, partly with future formalization in mind.

I understand that, under ordinary circumstances, one might be cautious about relying on a preprint that is only a few weeks old. In the present context, however, that caution seems less relevant: the goal here is formalization, which is arguably the strongest possible filter. What is more, I am here, and I would be very happy to answer questions and to cooperate with anyone interested in producing a detailed blueprint.

PS. [Büthe] contains some minor errors affecting the constants in the final result. They were later corrected in a Master’s thesis by S. Bhattacharjee (https://opus.uleth.ca/items/b6026465-4a9c-443a-b8e1-f2acd4068991).
PPS. I expect that [Büthe2] will also eventually be superseded by a cleaner argument based on the same general FFT-based idea, but that is future work and will take more time.

[Alex Kontorovich]

I'm just back from JMM, and eager to try out the new LeanArchitect system. Let me claim the first thing unclaimed: 3.a.9, and test things out. Thanks!

[Alex Kontorovich]

@Aaron Hill, have you made progress on 3a.8? There's a problem with the formalization, the indexing is off (in Lean, Fin 3 is $\{0,1,2\}$; it doesn't matter... until you use the index as an exponent!...). So I can't use exists_q_primes in the proof of prod_q_ge until we agree on the correct statement...

[Terence Tao]

I think in the formalization the indexing is consistently 0,1,2, even though the blueprint consistently states 1,2,3.

[Alex Kontorovich]

I may as well claim 3.a.10 and 3.a.11, since they're closely related. I'm remembering (thanks to @Pietro Monticone) that this is the kind of thing that I shouldn't do by hand but rather find which AI does it best. Good excuse to finally get Aristotle/AlphaProof/Logical Intelligence up and running on my end (I've been sitting on the API keys, but not yet trying them out).

[Terence Tao]

@Harald Helfgott Thanks for the suggestion! As discussed before, I am currently focused on formalizing FKS, but based on what you say, your new paper with Chirre would also be a natural target.

What I would need from you to help get that paper added into the workflow is to provide a LaTeX file containing the key theorems and proofs of your paper, arranged in a linear order with the theorem statements next to their proof: thus for instance if Theorem 1.1 requires Proposition 4.1 in its proof, then the statement and proof of Theorem 1.1 should appear after Proposition 4.1. (In particular, the main results of the paper would probably appear close to the end of the file, rather than close to the start.) I should be able to create a blueprint based on that ordered version of the paper. (Any side remarks in the paper that are not directly relevant to proving the theorems can be removed; the important thing is to have the theorem statements and proofs in order, which I would imagine would be an easier task for an author of the paper than an external reader.)

[Harald Helfgott]

@Terence Tao Do you prefer that to a flow diagram (in TikZ, say)? Also, any preference on whether I start with the $M(x)$ paper or the $\psi(x)$ paper?

[Terence Tao]

The LaTeX file could be more directly converted into a blueprint. A flow diagram would also be helpful to add metadata (which lemmas are used to prove which theorems) but this is secondary.

I'd say to start with whatever paper is shorter and/or more self-contained to get a hang of the workflow, in particular if there is some fragment of one paper which already attains an interesting result, one could start with formalizing just that and leave the rest of the paper for a later stage of the project.

[Alex Kontorovich]

Terence Tao said:

I think in the formalization the indexing is consistently 0,1,2, even though the blueprint consistently states 1,2,3.

Ah, it should be ok then. Should I fix the TeX (in these spots, to match the Lean), or will that break the TeX elsewhere and be annoying...?

[Terence Tao]

One would have to change the blueprint everywhere to reindex 1,2,3 by 0,1,2. Which is no big deal, though then the blueprint would differ from the original source material (the MathOverflow answer). So the question is where to draw the line between the 1-indexed convention and the 0-indexed convention. Certainly it would be silly to change the Lean to be 1-indexed since Mathlib is much more optimized for 0-indexed notations. My chosen compromise was to draw the line at the boundary between the informal blueprint and the formal Lean code, but we could move it elsewhere if there was consensus.

[Alex Kontorovich]

Task 3.a.9 is done, PNT#484 (ended up doing it the old fashioned way, just to get my bearings in LeanArchitect, which is indeed very similar to the previous workflow). There was indeed a minus sign missing from the statement of exists_q_primes.

[Alex Kontorovich]

Terence Tao said:

One would have to change the blueprint everywhere to reindex 1,2,3 by 0,1,2. Which is no big deal, though then the blueprint would differ from the original source material (the MathOverflow answer). So the question is where to draw the line between the 1-indexed convention and the 0-indexed convention. Certainly it would be silly to change the Lean to be 1-indexed since Mathlib is much more optimized for 0-indexed notations. My chosen compromise was to draw the line at the boundary between the informal blueprint and the formal Lean code, but we could move it elsewhere if there was consensus.

I see; it's perfectly fine to leave it as you have it. Maybe we should add a remark to the very beginning of the section with a warning that we've kept the TeX matching the original source, but the Lean doesn't match that?

[Alex Kontorovich]

And just so I'm clear: @Pietro Monticone, I don't need to mark anything as \leanok anymore, right? LeanArchitect will know to change the coloring automatically, since there's no sorry in the proof? Thanks!

[Pietro Monticone]

Yep

[Terence Tao]

The auto-coloring of the blueprint and management of the \leanok tags is very pleasant from the project maintainer side of things!

[Pietro Monticone]

With the discussion parameter we’ll be able to connect task issues being claimed with declarations so that people don’t need to look at the list of issues to know where they can contribute.

It will be available both in input (Lean source code) and in output (blueprint website and depgraph).

Just a native LeanBlueprint command, but for some reasons we’ve never ended up using it.

[Terence Tao]

By the way, the sign change in exists_q_primes ended up breaking the proof of Criterion.mk'. I will try to fix this manually.

[Alex Kontorovich]

Whoops! I didn't notice the red squiggle all the way at the bottom, sorry!

[Alex Kontorovich]

By the way, you're braver than me - I usually wait for the CI green checkmark before merging (to catch these kinds of things... but it does slow things down...)

[Terence Tao]

OK PNT#486 will mostly fix this but one now needs a new sorry to fill in Criterion.mk', namely

have hmid : √n * (1 + 1 / (log √n) ^ 3) ^ 3 < n * (1 + 1 / (log √n) ^ 3) ^ (-3:ℝ) := by sorry

but this should presumably be easy.

[Terence Tao]

Yes, I was impatient and merged before waiting for the CI. Will do that for the current PR :grinning_face_with_smiling_eyes:

[Alex Kontorovich]

Maybe I should flag @Aaron Hill one more time about the change in exists_q_primes -- it wasn't the reindexing that was the problem, but a missing minus sign, FYI.

[Aaron Hill]

I haven't started yet, so feel free to make whatever changes are helpful

[Harald Helfgott]

@Terence Tao All right - let me get back to you on that in a short while, since on of the two papers (the shorter one) is undergoing some restructuring.

In the meantime, I would like to get an idea of the level of granularity required in a blueprint (even though you are offering to produce a blueprint from a simple ordered outline, and I am gratefully accepting this offer). Here as an idea - should I start a thread in which I put up a Lemma (which is basic and self-contained but isn't completely dull) and people can tell me whether it would remain one lemma in the blueprint, or whether it would become several lemmas? It would also be a good way to discuss other matters - when to convert from reals to integers, how detailed the use of standard lemmas on exchanging sums and integrals (say) has to be in a blueprint, etc. Or is this not a good space for that?

[Pietro Monticone]

Terence Tao said:

OK PNT#486 will mostly fix this but one now needs a new sorry to fill in Criterion.mk', namely

have hmid : √n * (1 + 1 / (log √n) ^ 3) ^ 3 < n * (1 + 1 / (log √n) ^ 3) ^ (-3:ℝ) := by sorry

but this should presumably be easy.

Finished in PNT#488.

[Terence Tao]

@Harald Helfgott No immediate rush, as I imagine the two FKS papers will take up a lot of time and attention anyway.

I would imagine that ultimately a lemma in the paper may correspond to several sublemmas in the blueprint, but this type of refactoring is a relatively easy local edit to accomplish later in the process; the important thing is to get at least a coarse-scale blueprint online initially, and then further subdivision can be accomplished as needed. But you can certainly put up a lemma and I (and others) could comment on how it may be profitably decomposed into sublemmas. In general the finer grained, the better, but coarse-grained is still much better than no blueprint at all.

I should have mentioned that definitions - and particularly the "running hypotheses" that are in operation in any given section of the paper - are particularly valuable to make explicit in the blueprint. In my ongoing formalization of the FKS papers I am finding that often the conclusions of the theorem are not well defined in terms of the variables and parameters explicitly stated in the text of the theorem, because there are some ambient parameters and hypotheses that were introduced earlier in the paper and still considered to be in effect during the theorem in question. I have been able to fix these issues as part of the formalization process, but it would certainly have saved me some effort and confusion to have them explicit. This is not to say that every theorem should explicitly list over and over again all of the ambient parameters - that would be a lot of clutter - but having explicit definitions to the effect of "for the rest of Section 6, $H_0$ is understood to be a parameter such that ..." will be helpful. In Lean, one can create a structure with a name like AmbientParameters to hold all of this running data, and then each theorem in that section can reference a single instance of AmbientParameters to access all of the running variables and hypotheses. This tends to be pretty robust with respect to subsequent changes in the argument, for instance when one realizes that some additional side conditions on the parameters (e.g., positivity) are needed to make the proof go through.

[Harald Helfgott]

@Terence Tao Understood. Should I create a channel for this? Actually, once we are done with that Lemma, let us go one step further - I just wrote a self-contained short appendix proving an explicit version of a standard estimate; this is the sort of thing that people have proved several times with different constants, so we know it's useful, and this time the leading constant will be optimal.

[Terence Tao]

I think one can set up a discussion thread with a new topic within PNT+ for this. This type of self-contained appendix sounds like a great initial test case to create a mini-formalization project - a linearly ordered set of definitions, lemmas, and proofs would be enough to get an initial blueprint going I think.

[Harald Helfgott]

Just set up a thread for the lemma. I'll open a thread on the appendix tomorrow.

[Pietro Monticone]

Oh, Aristotle negated prod_p_ge:

theorem prod_p_ge {n : ℕ} (hn : n ≥ X₀ ^ 2) :
    ∏ i, (1 + (1 : ℝ) / ((exists_p_primes hn).choose i * ((exists_p_primes hn).choose i + 1))) ≥
      ∏ i : Fin 3, (1 + (1 + 1 / (log √(n : ℝ)) ^ 3) ^ (2 * (i : ℕ) + 2 : ℝ) * (n + √n)) := by
  sorry

So I checked and noticed a typo. The blueprint says:

$\prod_{i=1}^3 \Bigl(1 + \frac{1}{p_i(p_i+1)}\Bigr) \ge \prod_{i=1}^3 \Bigl(1 + \frac{1}{\bigl(1 + \frac{1}{\log^3 \sqrt{n}}\bigr)^{2i} (n + \sqrt{n})}\Bigr)$

The Lean statement was missing the 1 / on the right-hand side.

I'll open a PR with the following fix soon:

theorem prod_p_ge {n : ℕ} (hn : n ≥ X₀ ^ 2) :
    ∏ i, (1 + (1 : ℝ) / ((exists_p_primes hn).choose i * ((exists_p_primes hn).choose i + 1))) ≥
      ∏ i : Fin 3, (1 + 1 / ((1 + 1 / (log √(n : ℝ)) ^ 3) ^ (2 * (i : ℕ) + 2 : ℝ) * (n + √n))) := by
  sorry

[Pietro Monticone]

PNT#489

[Terence Tao]

@Snir Broshi I'm sorry, but due to some crossed wires it turns out that the lemma Criterion.q_not_dvd_L’ you were formalizing accidentally got formalized by one of my students. But if you were working on a Mathlib-appropriate lemma as discussed above, that could still be added to the project to be upstreamed at some point. I'll work with my students to make sure these sorts of collisions don't happen again.

[Snir Broshi]

Thanks for the heads up, no worries, I'm indeed working on Mathlib lemmas to upstream which should simplify the proof of it.
btw PNT#491 is much longer than I expected, I think the first 30 lines of it correspond to the first 3 lines in my PR. I might try to golf it instead then. (edit: PNT#493)

[Aayush Rajasekaran]

Alex Kontorovich said:

Task 3.a.9 is done, PNT#484 (ended up doing it the old fashioned way, just to get my bearings in LeanArchitect, which is indeed very similar to the previous workflow). There was indeed a minus sign missing from the statement of exists_q_primes.

@Alex Kontorovich FYI I attempted a minor golf of this PR here.

[Alex Kontorovich]

That's great, thanks! (For some stupid reason, ring_nf wasn't closing the goal. So a few calls to conv? and point-clicking did the trick... Though of course it looked very ugly.)