Starting on BKLNW

Stream: PrimeNumberTheorem+

[Terence Tao]

I was vaguely aware that each paper in the field of explicit analytic number theory tends to rely rather crucially on prior papers in the field, and FKS2 is no exception. In addition to using the identities of Rosser and Schoenfeld, they also use a prior paper of Broadbent, Kadiri, Lumley, Ng, and Wilk (BKLNW) that,, among other things, provides very explicit bounds for the error $\psi(x) - \theta(x)$ between the two Chebyshev functions $\psi$, $\theta$, with the difference coming from squares and higher powers of primes. So, to fully formalize the final statements of FKS2, one needs at some point to formalize a fair chunk of BKLNW.

The process is now started in a sequence of small tasks PNT#629 PNT#630 PNT#631 PNT#632 PNT#633 PNT#634 PNT#635 PNT#636 PNT#637 PNT#639 PNT#640 PNT#641 PNT#642 PNT#643. These tasks take a bunch of inputs (stored in a custom Inputs structure) assuming various bounds on $\theta(x)$, and uses this (and the obvious formula $\psi(x) = \theta(x) + \theta(x^{1/2}) + \theta(x^{1/3}) + \dots$) to obtain good bounds on $\psi(x) - \theta(x)$. These are rather routine, unsurprising estimates, but they do require a fair amount of bookkeeping. (The input estimates themselves rely on previous papers, some of which are extremely computational, but I will defer consideration of how to justify them for some later date.)

I have been dumping quite a few issues now into the project, but my expectation is that many of them are rather easy and can be dealt with either by humans or AI tools in relatively short order. Still a ways to go before we can formalize an end-to-end explicit prime number theorem, but the workflow seems to beoming clearer at least.

[Harald Helfgott]

Right. In 'civilian life' - that is, outside this project - I have been trying to minimize my dependence on this entire tradition in the last few years. That said, while I think by now (thanks to my very recent preprints with Chirre) I would be able to redo ternary Goldbach without using any results of type $\psi(x) - x = o(x)$ or $M(x) = o(x)$, even indirectly -- and that was part of the goal -- I really do think a (good) result of type $\psi(x)-x = o(x)$ is essential for the field -- and that formalization is a priority, precisely for the reasons you mention. Of course one will then be able to combine it with bounded-functions Chirre-Helfgott to get a strong $M(x) = o(x)$ result.

[Aayush Rajasekaran]

@Terence Tao Dumping issues is good, it's great to have accessible stuff to work on.

Here is a PR for PNT#635

[Aayush Rajasekaran]

Here is a PR for PNT#632

[Aayush Rajasekaran]

Here is a PR for PNT#638

And here is a PR for PNT#637

[Aayush Rajasekaran]

main is currently broken because the proof of prop_3_sub_8 landed before the fixup of prop_3_sub_7. This PR should fix it again.

[Yongxi Lin (Aaron)]

I am working on PNT#641 right now. In the paper, the authors assume $b\ge7$ in proposition 4, while we don't have this requirement in the definition of Inputs. Is that a typo?

I am also not sure about the second part of case 1. We want to prove the strict inequality
$\theta(x^{1/2})<(1+\epsilon(\log x_1))x^{1/2}$, but the paper only proves the nonstrict inequality for $x^{1/2}>x_1$.

[Terence Tao]

Oops, you are right, the hypothesis $b \geq 7$ probably needs to be added in Proposition 4 and possibly some of its sublemmas too, since this hypothesis is required for Corollary 3.1.

Looking at the paper I agree that the argument actually only shows non-strict inequality rather than strict inequality. Technically this is an error in the paper, but I assume it won't change the final bounds all that much (probably at worst some other strict inequalities become non-strict). For now, perhaps just change all strict inequalities to non-strict inequalities and hope that this doesn't force too many downstream lemmas to also change in this manner.

[Terence Tao]

Oh, one additional thing: if you do find that you have to deviate from the published version of the text, make a note of this in the blueprint text for the record, so that the discrepancy between the Lean code and the published paper can be explained to future readers.

[Yongxi Lin (Aaron)]

PNT#726 has a proof for PNT#634. However, in order to make it work I need to increase maxHeartbeats. Are there any ways to golf it so that it requires fewer heartbeats?

[Ruben Van de Velde]

Running nlinarith in what, 120 subgoals? sounds disastrous

[Terence Tao]

I've realized that I need to do some significant refactoring of BKLNW as I had misunderstood the flow of logic in the paper; the ordering of the theorems in the file will be permuted quite a bit, and the Inputs structure will need to be broken up into several different types of inputs (in particular I have now realized that the purpose of some of the theorems in the paper is to turn one claim that is currently a component of Inputs into another component of Inputs, which defeats the purpose of having one single Inputs structure to hold all these claims). The issues that have already been claimed will still be usable, but for now I am putting the note "DO NOT CLAIM" on all currently unclaimed BKLNW tasks. Once all the claimed ones are completed, I will do the refactoring and then release the tasks for BKLNW to be claimed again (and add some new ones).

For those of you who have already claimed a BKLNW task, don't worry - keep proceeding as before, I will wait until they are all processed before doing the refactoring (to avoid creating a massive number of merge conflicts).

[Lawrence Wu (llllvvuu)]

Yongxi Lin (Aaron) said:

PNT#726 has a proof for PNT#634. However, in order to make it work I need to increase maxHeartbeats. Are there any ways to golf it so that it requires fewer heartbeats?

One way to vibe-prove a computation like this could be to fix the computational part to something efficient, like this:

import Mathlib

open Real Set

noncomputable def u (n : ℕ) : ℝ := ∑ k ∈ Finset.Icc 4 n, 2 ^ ((n / k : ℝ) - (n / 3 : ℝ))

noncomputable def summand (k n : ℕ) : ℝ :=
  (2 : ℝ) ^ ((n + 1 : ℝ) / k) * ((2 : ℝ) ^ (1 / 3 - 1 / k : ℝ) - 1)

lemma summand_pos.aux {k : ℕ} (hk : 3 < k) (n : ℕ) : 0 < (2 : ℝ) ^ (1 / 3 - 1 / k : ℝ) - 1 := by
  sorry

lemma summand_pos {k : ℕ} (hk : 3 < k) (n : ℕ) : 0 < summand k n := by
  sorry

lemma summand_mono {k : ℕ} (hk : 3 < k) : StrictMono (summand k) := by
  sorry

lemma sum_gt.aux (k : ℕ) (a b : ℝ) (hk : 3 < k := by decide) (hb1 : 0 ≤ b - 1 := by norm_num only)
    (ha : a ^ k ≤ 1024 := by norm_num only) (hb : b ^ (3 * k) ≤ 2 ^ (k - 3) := by norm_num only) :
    a * (b - 1) ≤ summand k 9 := by
  have ha_bound : a ≤ 2 ^ (10 / k : ℝ) := by sorry
  have hb_bound : b - 1 ≤ 2 ^ (1 / 3 - 1 / k : ℝ) - 1 := by sorry
  grw [ha_bound, hb_bound]
  norm_num [summand]

lemma sum_gt {n : ℕ} (hn : 9 ≤ n) : 2.12 < ∑ k ∈ Finset.Icc 4 n, summand k n := calc
  _ < ∑ k ∈ Finset.Icc 4 9, summand k 9 := by
    simp only [Nat.reduceLeDiff, Finset.sum_Icc_succ_top, Finset.Icc_self, Finset.sum_singleton]
    grw [← sum_gt.aux 4 5.65 1.05, ← sum_gt.aux 5 4 1.09, ← sum_gt.aux 6 3.17 1.12,
      ← sum_gt.aux 7 2.69 1.14, ← sum_gt.aux 8 2.37 1.155, ← sum_gt.aux 9 2.16 1.1665]
    norm_num
  _ ≤ ∑ k ∈ Finset.Icc 4 n, summand k 9 := by sorry
  _ ≤ _ := Finset.sum_le_sum fun k hk ↦ (summand_mono (by grind)).le_iff_le.mpr hn

lemma u_diff_factored {n : ℕ} (hn : 4 ≤ n) :
    u (n + 1) - u n = 2 ^ (-(n + 1) / 3 : ℝ) * (2 - ∑ k ∈ Finset.Icc 4 n, summand k n) := by
  sorry

theorem prop_3_sub_4 (n : ℕ) (hn : 9 ≤ n) : u (n + 1) < u n := by
  grw [← sub_neg, u_diff_factored (by grind), ← sum_gt hn]
  norm_num
  positivity

and let AI do the rest.

[Terence Tao]

An update on the refactoring. I have isolated one of the key problems: BKLNW has a large appendix (Appendix A) which has different inputs and outputs than the main paper. In particular, one of the main outputs of Appendix A, namely Theorem 2, is a key input for the rest of the paper. This created some confusion for me when I tried to assign a unified set of inputs and outputs for the combined paper. The logical solution is to create a new Lean file BKLNW_app.Lean to formalize the appendix only, with its own inputs and outputs, and import it into BKLNW.lean, which will now be a somewhat simpler file with a separate set of inputs and outputs. This, together with some further reorganization of the remaining BKLNW theorems, should resolve the dependency issues I was facing before. Fortunately, I can go start working on the appendix independently of the existing tasks to formalize some non-appendix BKLNW papers, so the contributors working on BKLNW tasks should not feel pressured to finish early!

[Terence Tao]

@Lawrence Wu (llllvvuu) This is a nice argument, and a bit simpler than the one provided in the paper. Did you find it by pen and paper (or some separate numerical calculation) first?

[Yongxi Lin (Aaron)]

@Lawrence Wu (llllvvuu) Thank you for your execellent golf! I just merged your proof into PNT#726, which is ready to be reviewed now.

[Lawrence Wu (llllvvuu)]

My process was:

• Perceive the computational issue as evaluating a different number terms for each n. What if we just evaluate once the maximal number of terms needed? This would be at n=9. At this point I realized that by the original monotonicity argument, the n=9 sum is actually a bound for the general n sum.
• Now examine the summand and notice the rational powers which means we can use integer comparison. Extract this into a lemma (to be proved by Aristotle) so that the summand lower bounds can be "automated" with autoParams.
• I used a calculator for the 2^(p/q) estimates. For the overall sum estimate (2.12) I just tweaked it in Lean to get it passing (manual binary search) although I could have also pasted from the infoview into a calculator.

I didn't check the calculation beforehand. I just assumed that, since the statement is true and the 2^(p/q) estimates are arbitrarily precise, it would work out and Lean would check it.

[Terence Tao]

BKLNW is now refactored! All previous issues are now claimable, and I am now also adding a few more tasks to the queue: PNT#787 PNT#788 PNT#789 PNT#790 PNT#791

[Harald Helfgott]

On PNT #787 (importing equation (1.7) from Büthe's "An analytic method..."): that is, in a sense, a safe thing to import, in that it's certainly true, and something that can be proved. I don't necessarily recommend formalizing that paper by Büthe, though it's really your choice. The central idea is sound, viz., use FFT. Just be aware that there are better ways to do it.

[Terence Tao]

Would your forthcoming paper serve as a substitute for Buthe's results? They are used as inputs to BKLNW, which are in turn inputs to FKS2, mostly to cover medium ranges of $x$.

[Harald Helfgott]

That depends on the meaning of forthcoming. I have two very recent preprints in the arXiv, the second of which replaces Büthe's other paper, among other things.

As for Büthe's "An analytic method...", which is what is relevant here: what you will find in section 9.4 of the first preprint is a very brief sketch of the main idea of what I believe is a cleaner and more effective way to execute the FFT strategy. I'll be glad to give some details if needed.

The frank answer would be: the replacement for Büthe's "An analytic paper..." is in a paper I haven't written yet. Since it would have a serious computational part, it may be best to team up with a strong (and interested) computational collaborator.

[Pietro Monticone]

Aristotle has disproved thm_1a_table and proposed the following fix:

noncomputable section AristotleLemmas

def BKLNW.check_row_prop (row : ℝ × ℝ × ℝ) : Prop :=
  let b := row.1
  let M := row.2.1
  let m := row.2.2
  20 ≤ b ∧
  BKLNW.Pre_inputs.default.ε b ≤ M ∧
  BKLNW.Pre_inputs.default.ε b + RS_prime.c₀ * (Real.exp (-b/2) + Real.exp (-2*b/3) + Real.exp (-4*b/5)) ≤ m

lemma BKLNW.check_row_implies_bound {b M m : ℝ} (h : BKLNW.check_row_prop (b, M, m)) {x : ℝ} (hx : x ≥ Real.exp b) :
    x * (1 - m) ≤ θ x ∧ θ x ≤ x * (1 + M) := by
      obtain ⟨ hb, hM, hm ⟩ := h;
      have := BKLNW.thm_1a ( show Real.exp b ≥ Real.exp 20 by exact Real.exp_le_exp.mpr hb ) ( show Real.exp b ≥ Real.exp 20 by exact Real.exp_le_exp.mpr hb ) ( show x ≥ Real.exp b by linarith ) ( show x ≥ Real.exp b by linarith );
      norm_num [ Real.rpow_def_of_pos ( Real.exp_pos _ ) ] at *;
      constructor <;> ring_nf at * <;> nlinarith [ Real.exp_pos b ]

theorem BKLNW.thm_1a_table_corrected {b M m : ℝ} (h : (b, M, m) ∈ BKLNW.Table_14) (h_check : BKLNW.check_row_prop (b, M, m)) {x : ℝ} (hx : x ≥ Real.exp b) :
    x * (1 - m) ≤ θ x ∧ θ x ≤ x * (1 + M) := by
  apply BKLNW.check_row_implies_bound h_check hx

lemma BKLNW.row_1_checked : BKLNW.check_row_prop (20, 4.2676e-5, 9.1639e-5) := by
  unfold BKLNW.check_row_prop BKLNW.Pre_inputs.default BKLNW_app.table_8_ε RS_prime.c₀
  norm_num
  rw [Real.exp_neg, Real.exp_neg, Real.exp_neg]
  -- We assume the inequality holds by calculation
  -- We'll use the exponential property to simplify the expression. Note that $(e^{10})^{-1} = e^{-10}$, $(e^{40/3})^{-1} = e^{-40/3}$, and $(e^{16})^{-1} = e^{-16}$.
  suffices h_exp : (4267 / 100000000 : ℝ) + (103883 / 100000) * (Real.exp (-10) + Real.exp (-40 / 3) + Real.exp (-16)) ≤ 91639 / 1000000000 by
    convert h_exp using 1 ; norm_num [ Real.exp_neg ];
  field_simp;
  have := Real.exp_neg_one_lt_d9 ; norm_num1 at * ; rw [ show Real.exp ( -10 ) = ( Real.exp ( -1 ) ) ^ 10 by rw [ ← Real.exp_nat_mul ] ; ring, show Real.exp ( - ( 40 / 3 ) ) = ( Real.exp ( -1 ) ) ^ ( 40 / 3 : ℝ ) by rw [ ← Real.exp_mul ] ; ring, show Real.exp ( -16 ) = ( Real.exp ( -1 ) ) ^ 16 by rw [ ← Real.exp_nat_mul ] ; ring ];
  -- Substitute the upper bound for exp(-1) into the expression.
  have h_sub : (426700000 + 10388300000000 * ((919698603 / 2500000000 : ℝ) ^ 10 + (919698603 / 2500000000 : ℝ) ^ (40 / 3 : ℝ) + (919698603 / 2500000000 : ℝ) ^ 16)) * 1000000000 ≤ 916390000000000000 := by
    rw [ show ( 40 / 3 : ℝ ) = 13 + 1 / 3 by norm_num, Real.rpow_add ] <;> norm_num;
    -- Let $y = (919698603 / 2500000000)^{1/3}$. Then we have $y^3 = 919698603 / 2500000000$.
    set y : ℝ := (919698603 / 2500000000 : ℝ) ^ (1 / 3 : ℝ)
    have hy3 : y^3 = 919698603 / 2500000000 := by
      rw [ ← Real.rpow_natCast, ← Real.rpow_mul ] <;> norm_num;
    nlinarith [ sq_nonneg ( y^2 ) ];
  exact le_trans ( by gcongr ) h_sub

end AristotleLemmas

/-
See [reference] for values of $m_0$ and $M_0$.
-/
theorem thm_1a_table {X₀ m₀ M₀ : ℝ} (h : (X₀, M₀, m₀) ∈ Table_14) {x : ℝ} (hx : x ≥ X₀) :
  x * (1 - m₀) ≤ θ x ∧ θ x ≤ x * (1 + M₀) :=
  by
    -- Wait, there's a mistake. We can actually prove the opposite.
    negate_state;
    -- Proof starts here:
    -- Choose $X₀ = 20$, $m₀ = 9.1639e-5$, and $M₀ = 4.2676e-5$.
    use 20, 9.1639e-5, 4.2676e-5;
    -- Now show that the chosen values satisfy the conditions.
    constructor <;> norm_num [BKLNW.Table_14] at *;
    -- Choose $x = 20$.
    use 20; norm_num [BKLNW.Table_14] at *; (
    -- Let's calculate the value of $\theta(20)$ and show that it is less than $250010669 / 12500000$.
    have h_theta_20 : θ 20 = ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc 2 20), Real.log p := by
      -- By definition of θ, we have θ(20) = ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc 2 20), Real.log p.
      simp [theta] at *; (
      rfl)
    rw [h_theta_20] ; norm_num [Finset.sum_filter, Finset.sum_Ioc_succ_top, (Nat.succ_eq_succ ▸ Finset.Icc_succ_left_eq_Ioc)] at * ; (
    -- We'll use that $Real.log 2 \approx 0.693147$, $Real.log 3 \approx 1.098612$, $Real.log 5 \approx 1.609438$, $Real.log 7 \approx 1.945910$, $Real.log 11 \approx 2.397895$, $Real.log 13 \approx 2.564949$, $Real.log 17 \approx 2.833213$, and $Real.log 19 \approx 2.944439$.
    have h_log_approx : Real.log 2 < 0.7 ∧ Real.log 3 < 1.1 ∧ Real.log 5 < 1.7 ∧ Real.log 7 < 2 ∧ Real.log 11 < 2.4 ∧ Real.log 13 < 2.6 ∧ Real.log 17 < 2.9 ∧ Real.log 19 < 3 := by
      refine' ⟨ Real.log_two_lt_d9.trans_le <| by norm_num, _, _, _, _, _, _, _ ⟩ <;> norm_num [ Real.log_lt_iff_lt_exp ] at *;
      any_goals have := Real.exp_one_gt_d9.le; norm_num at *; rw [ show Real.exp 3 = ( Real.exp 1 ) ^ 3 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; nlinarith [ pow_le_pow_left₀ ( by positivity ) this 3 ] ;
      any_goals have := Real.exp_one_gt_d9.le; norm_num at *; rw [ show Real.exp ( 2 : ℝ ) = ( Real.exp 1 ) ^ 2 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; nlinarith [ Real.add_one_le_exp 1 ] ;
      · -- We can raise both sides to the power of 10 to remove the fraction.
        have h_exp : (3 : ℝ) ^ 10 < Real.exp 11 := by
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 11 = ( Real.exp 1 ) ^ 11 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; nlinarith [ pow_le_pow_left₀ ( by positivity ) this 11 ] ;
        exact lt_of_pow_lt_pow_left₀ _ (by positivity) (h_exp.trans_le (by norm_num [ ← Real.exp_nat_mul ]));
      · -- We can raise both sides to the power of 10 to get $5^{10} < e^{17}$.
        have h_exp : (5 : ℝ) ^ 10 < Real.exp 17 := by
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 17 = ( Real.exp 1 ) ^ 17 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ ) ;
        contrapose! h_exp;
        exact le_trans ( by norm_num [ ← Real.exp_nat_mul ] ) ( pow_le_pow_left₀ ( by positivity ) h_exp 10 );
      · -- We can raise both sides to the power of 5 to get $11^5 < e^{12}$.
        have h_exp : (11 : ℝ)^5 < Real.exp 12 := by
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 12 = ( Real.exp 1 ) ^ 12 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; nlinarith [ pow_le_pow_left₀ ( by positivity ) this 12 ] ;
        contrapose! h_exp;
        exact le_trans ( by norm_num [ ← Real.exp_nat_mul ] ) ( pow_le_pow_left₀ ( by positivity ) h_exp 5 );
      · -- We can raise both sides to the power of 5 to get $13^5 < e^{13}$.
        have h_exp : (13 : ℝ)^5 < Real.exp 13 := by
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 13 = ( Real.exp 1 ) ^ 13 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ ) ;
        generalize_proofs at *; (
        contrapose! h_exp; rw [ show Real.exp 13 = ( Real.exp ( 13 / 5 ) ) ^ 5 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact pow_le_pow_left₀ ( by positivity ) h_exp 5;);
      · -- We can raise both sides to the power of 10 to get $17^{10} < e^{29}$.
        have h_exp : (17 : ℝ) ^ 10 < Real.exp 29 := by
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 29 = ( Real.exp 1 ) ^ 29 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ ) ;
        contrapose! h_exp;
        exact le_trans ( by norm_num [ ← Real.exp_nat_mul ] ) ( pow_le_pow_left₀ ( by positivity ) h_exp 10 );
    exact fun h => by norm_num1 at *; linarith;))

[Terence Tao]

Ah, so I forgot to exponentiate the lower bound? I agree with this fix.

[Pietro Monticone]

I'll open a PR soon.

[Pietro Monticone]

There is not a task issue for that one yet, right? @Terence Tao

[Terence Tao]

No, I was planning to add it today. I can wait for your PR of course.

[Pietro Monticone]

I'll add the discussion parameter. Could you please open the task issue?

[Terence Tao]

OK, I'll do that now.

[Terence Tao]

PNT#801. This will be the first of several "By the previous theoretical result, we get explicit numerical results according to <Table of 100 values of parameters>". I'm hoping that automated tools can handle this sort of thing, because this would be extremely tedious to do by hand.

[Pietro Monticone]

Opened PNT#804 closing PNT#801.

[Terence Tao]

That was surprisingly short. So all the numerical verification is being pushed to a proposition check_row_prop, but that the fact that the entries in Table_14 obey this proposition is not yet formalized?

[Pietro Monticone]

We need to add another sorried theorem

[Terence Tao]

Ah OK. Would you be willing to add that within the PR?

[Pietro Monticone]

Oh, wait, are you referring to:

lemma BKLNW.row_1_checked : BKLNW.check_row_prop (20, 4.2676e-5, 9.1639e-5) := by
  unfold BKLNW.check_row_prop BKLNW.Pre_inputs.default BKLNW_app.table_8_ε RS_prime.c₀
  norm_num
  rw [Real.exp_neg, Real.exp_neg, Real.exp_neg]
  -- We assume the inequality holds by calculation
  -- We'll use the exponential property to simplify the expression. Note that $(e^{10})^{-1} = e^{-10}$, $(e^{40/3})^{-1} = e^{-40/3}$, and $(e^{16})^{-1} = e^{-16}$.
  suffices h_exp : (4267 / 100000000 : ℝ) + (103883 / 100000) * (Real.exp (-10) + Real.exp (-40 / 3) + Real.exp (-16)) ≤ 91639 / 1000000000 by
    convert h_exp using 1 ; norm_num [ Real.exp_neg ];
  field_simp;
  have := Real.exp_neg_one_lt_d9 ; norm_num1 at * ; rw [ show Real.exp ( -10 ) = ( Real.exp ( -1 ) ) ^ 10 by rw [ ← Real.exp_nat_mul ] ; ring, show Real.exp ( - ( 40 / 3 ) ) = ( Real.exp ( -1 ) ) ^ ( 40 / 3 : ℝ ) by rw [ ← Real.exp_mul ] ; ring, show Real.exp ( -16 ) = ( Real.exp ( -1 ) ) ^ 16 by rw [ ← Real.exp_nat_mul ] ; ring ];
  -- Substitute the upper bound for exp(-1) into the expression.
  have h_sub : (426700000 + 10388300000000 * ((919698603 / 2500000000 : ℝ) ^ 10 + (919698603 / 2500000000 : ℝ) ^ (40 / 3 : ℝ) + (919698603 / 2500000000 : ℝ) ^ 16)) * 1000000000 ≤ 916390000000000000 := by
    rw [ show ( 40 / 3 : ℝ ) = 13 + 1 / 3 by norm_num, Real.rpow_add ] <;> norm_num;
    -- Let $y = (919698603 / 2500000000)^{1/3}$. Then we have $y^3 = 919698603 / 2500000000$.
    set y : ℝ := (919698603 / 2500000000 : ℝ) ^ (1 / 3 : ℝ)
    have hy3 : y^3 = 919698603 / 2500000000 := by
      rw [ ← Real.rpow_natCast, ← Real.rpow_mul ] <;> norm_num;
    nlinarith [ sq_nonneg ( y^2 ) ];
  exact le_trans ( by gcongr ) h_sub

?

[Terence Tao]

Yeah, that's the kind of thing I was expecting to see in PNT#804 but didn't. Hmm, but having one of these for each row could be computationally expensive. For some applications, only one row is needed, but there are some omnibus theorems where the table (which has about 25 rows) is being used. Perhaps one could move these numerics to a separate file that could be compiled once but would not be touched ever again so that one could rely on the cached olean file (if that's the right terminology)?

[Terence Tao]

Oh, now I see you did do row 1 in PNT#804. So... maybe an import that does nothing but check the arithmetic for rows 1-25? One may have to push Table_14 into that file to make it self-contained.

[Pietro Monticone]

For some reason I forgot to push that :man_facepalming:

[Pietro Monticone]

Ok, maybe I can push this one in PNT#804 and then we can "generalise".

[Terence Tao]

OK, I'll study your PR and propose a refactoring where there is some supplemental file BKNLW_table_14.lean that defines Table_14, check_row_prop, and proves a theorem Table_14.row_prop that every row in Table_14 obeys check_row_prop. This file could be lengthy due to the number of rows but my hope is that it would be very stable and self-contained (not importing anything else from PNT+) and ideally only need to be compiled once per Mathlib bump. The main BKLNW.lean file would then import BKNLW_table_14.lean and use Table_14.row_prop to prove the original theorem of PNT#801. Hopefully that makes sense.

[Pietro Monticone]

It sounds good. I hope BKNLW_table_14.lean will be completely filled by... non-humans

[Terence Tao]

Yeah, this is precisely the type of formalization one wants to offload completely to the robots.

[Pietro Monticone]

I'll submit it to Aristotle as soon as it's ready.

[Pietro Monticone]

PNT#804 is ready for review

[Lawrence Wu (llllvvuu)]

I'm not sure if table_8_ε is strong enough to give Table_14. For example, for b=35, it gives only 2.36034e-8 while Table_14 wants 2.3603e-8. Perhaps trickier is that it gives nothing between b=50 and b=100, we have in table_8_ε:

  else if b < 50 then 1.09073e-8
  else if b < 100 then 1.11990e-9
  else if b < 200 then 2.45299e-12

but in Table_14:

  (50, 1.1199e-9, 1.1344e-9),
  (60, 1.2215e-11, 1.2312e-11),
  (70, 2.7923e-12, 2.7930e-12),
  (80, 2.6108e-12, 2.6108e-12),
  (90, 2.5213e-12, 2.5213e-12),
  (100, 2.4530e-12, 2.4530e-12),

[Lawrence Wu (llllvvuu)]

In any case, the following technique (generated from a Python script from Claude Code) can check integer b up to the first 8 rows:

lemma check_row_prop_aux (b' : ℕ) (b p q r : ℝ) (hb : b = b' := by norm_num only)
    (hp0 : 0 ≤ p := by norm_num only)
    (hq0 : 0 ≤ q := by norm_num only)
    (hr0 : 0 ≤ r := by norm_num only)
    (hp : (0.3678794412 : ℝ) ^ b' ≤ p ^ 2 := by norm_num only)
    (hq : (0.3678794412 : ℝ) ^ (2 * b') ≤ q ^ 3 := by norm_num only)
    (hr : (0.3678794412 : ℝ) ^ (4 * b') ≤ r ^ 5 := by norm_num only) :
    RS_prime.c₀ * (exp (-b / 2) + exp (-2 * b / 3) + exp (-4 * b / 5)) ≤
    RS_prime.c₀ * (p + q + r) := by
  have h1 : exp (-b / 2) ≤ p := by
    rw [← pow_le_pow_iff_left₀ (by positivity) hp0 two_pos.ne', ← exp_nat_mul, hb, Nat.cast_ofNat]
    field_simp
    grw [← neg_one_mul, exp_mul, exp_neg_one_lt_d9]
    norm_cast
  have h2 : exp (-2 * b / 3) ≤ q := by
    rw [← pow_le_pow_iff_left₀ (by positivity) hq0 three_pos.ne', ← exp_nat_mul, hb, Nat.cast_ofNat]
    field_simp
    grw [← neg_one_mul, exp_mul, exp_neg_one_lt_d9]
    norm_cast
  have h3 : exp (-4 * b / 5) ≤ r := by
    rw [← pow_le_pow_iff_left₀ (by positivity) hr0 (by positivity : 5 ≠ 0),
      ← exp_nat_mul, hb, Nat.cast_ofNat]
    field_simp
    grw [← neg_one_mul, exp_mul, exp_neg_one_lt_d9]
    norm_cast
  have : 0 ≤ RS_prime.c₀ := by norm_num only [RS_prime.c₀]
  grw [h1, h2, h3]

lemma row_1_checked : check_row_prop (20, 4.2676e-5, 9.1639e-5) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 20 20 4.53999298e-5 1.61959680e-6 1.12535175e-7]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

lemma row_2_checked : check_row_prop (25, 3.5031e-6, 7.4366e-6) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 25 25 3.72665318e-6 5.77774853e-8 2.06115363e-9]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

lemma row_3_checked : check_row_prop (30, 2.8755e-7, 6.0751e-7) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 30 30 3.05902321e-7 2.06115363e-9 3.77513456e-11]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

lemma row_4_checked : check_row_prop (35, 2.36034e-8, 4.9766e-8) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 35 35 2.51099916e-8 7.35295808e-11 6.91440013e-13]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

lemma row_5_checked : check_row_prop (40, 1.9338e-8, 2.1482e-8) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 40 40 2.06115363e-9 2.62309378e-12 1.26641656e-14]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

lemma row_7_checked : check_row_prop (45, 1.09073e-8, 1.1084e-8) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 45 45 1.69189793e-10 9.35762300e-14 2.31952284e-16]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

lemma row_8_checked : check_row_prop (50, 1.1199e-9, 1.1344e-9) := by
  dsimp only [check_row_prop]
  grw [check_row_prop_aux 50 50 1.38879439e-11 3.33823781e-15 4.24835427e-18]
  norm_num [Pre_inputs.default, BKLNW_app.table_8_ε, RS_prime.c₀]

After this, it has the issue mentioned above, in addition to a minor issue that norm_num will not exponentiate further than 256:

example (x : ℝ) : (0.3678794412 : ℝ) ^ (256 : ℕ) = x := by norm_num; sorry
example (x : ℝ) : (0.3678794412 : ℝ) ^ (257 : ℕ) = x := by norm_num; sorry

but this should be easily circumventable by exponentiating twice:

example (x : ℝ) : ((0.3678794412 : ℝ) ^ (256 : ℕ)) ^ (8 : ℕ) = x := by norm_num; sorry

although it starts to get quite slow, so probably the precision should be reduced after the first exponentiation

[Terence Tao]

Aha! On Page 26 of https://arxiv.org/pdf/2002.11068 it is written, "The tables in this appendix are subsets of longer tables that can be found in the accompanying document [2]. Several results in this article make use of the longer tables.". This is https://arxiv.org/src/2002.11068v2/anc/Full-Tables-Sharper-Bounds-June-2020.pdf , see in particular the expanded Table 8 on pages 2-7. I will work in incorporating this expanded table.

[Terence Tao]

OK done. (Github Copilot is a lifesaver for this sort of data conversion.). Creating the PR PNT#806 to do the refactoring, if it compiles I will issue a task to verify row_prop for everything in Table_14 using the expanded Table_8.

[Terence Tao]

OK, I have refactored some of the tables into their own ecosystem of Lean files with much fewer imports. There are now two tasks PNT#807 PNT#808: the first is to show that the short version of Table 8 (which was already used in a couple places in the project) is weaker than the long version; and the second is to show that the long version of Table 8 can be used to verify the required conditions for Table 14.

[Pietro Monticone]

Aristotle has just negated table_8_ε.le_simp as follows:

/-
Check if the inequality fails at b=20.
-/
lemma check_disproof : BKLNW_app.table_8_ε 20 > BKLNW_app.table_8_ε' 20 := by
  norm_num [ BKLNW_app.table_8_ε, BKLNW_app.table_8_ε' ] at *;
  refine' lt_of_lt_of_le _ ( le_csInf _ _ );
  rotate_left;
  exact 4267 / 100000000 + 1 / 1000000000000;
  · exact ⟨ _, ⟨ 20, List.mem_cons.mpr ( Or.inl rfl ), by norm_num ⟩ ⟩;
  · norm_num +zetaDelta at *;
    intro b x hx hx'; fin_cases hx <;> norm_num at * ;
  · grind

end AristotleLemmas

/-
**BKLNW Table 8 vs expanded Table 8**

The value of $\eps(b)$ arising from Table 8 of [reference] is weaker than that from the expanded version of Table 8 available in the arXiv.
-/
theorem table_8_ε.le_simp (b : ℝ) (hb : b ≥ 20) : table_8_ε b ≤ table_8_ε' b := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- By definition of $table_8_ε'$, we know that for $b = 20$, $table_8_ε' 20 = 4.2670e-5$.
  use 20
  simp [check_disproof]

[Terence Tao]

Haha, on checking against the source material I see there is a typo in the first non-trivial line of table_8_ε': 4.2670e-5 should be 4.26760e-5. The amusing thing is that the first line was entered in by myself, and the subsequent lines filled in by Github Copilot (using a text dump of the original paper): so the error is a human error, but spot checks seem to confirm that all the AI-generated lines of the table are correct. Sometimes humans "hallucinate" too! :grinning_face_with_smiling_eyes:

Anyway, if you are working on this then perhaps you can fix the typo.

[Pietro Monticone]

Yes, I'll fix it in a PR soon.

[Pietro Monticone]

Opened PNT#810.

[Pietro Monticone]

Aristotle disproved the following:

theorem table_14_check {b M m : ℝ} (h_table : (b, M, m) ∈ Table_14) : check_row_prop (b, M, m) := by sorry

[Pietro Monticone]

In particular:

noncomputable section AristotleLemmas

/-
A helper lemma that simplifies checking the row property by using the computable upper bound `table_8_ε'` instead of the definition `table_8_ε`.
-/
lemma BKLNW.check_row_prop_of_simp {b M m : Real} (h20 : 20 ≤ b)
    (hM : BKLNW_app.table_8_ε' b ≤ M)
    (hm : BKLNW_app.table_8_ε' b + RS_prime.c₀ * (Real.exp (-b / 2) + Real.exp (-2 * b / 3) + Real.exp (-4 * b / 5)) ≤ m) :
    BKLNW.check_row_prop (b, M, m) := by
  simp only [BKLNW.check_row_prop]
  refine ⟨h20, ?_, ?_⟩
  · apply le_trans (BKLNW_app.table_8_ε.le_simp b h20) hM
  · apply le_trans _ hm
    apply add_le_add_right
    apply BKLNW_app.table_8_ε.le_simp b h20

/-
Check the row with `19 * log 10`.
-/
lemma BKLNW.check_row_log : BKLNW.check_row_prop (19 * Real.log 10, 1.9338e-8, 1.9667e-8) := by
  convert BKLNW.check_row_prop_of_simp _ _ _ using 1 <;> norm_num;
  · rw [ ← div_le_iff₀' ] <;> norm_num [ Real.le_log_iff_exp_le ];
    have := Real.exp_one_lt_d9.le ; norm_num at * ; rw [ show ( 20 : ℝ ) / 19 = 1 + ( 1 / 19 ) by norm_num, Real.exp_add ] ; nlinarith [ Real.exp_pos ( 1 / 19 ), Real.exp_neg ( 1 / 19 ), mul_inv_cancel₀ ( ne_of_gt ( Real.exp_pos ( 1 / 19 ) ) ), Real.add_one_le_exp ( 1 / 19 ), Real.add_one_le_exp ( - ( 1 / 19 ) ) ] ;
  · rw [ show BKLNW_app.table_8_ε' ( 19 * Real.log 10 ) = 1.93378e-8 by
          -- Since $19 * \log 10$ is approximately $43.7$, it falls into the interval $40 \leq b < 45$, where the value is $1.93378e-8$.
          have h_interval : 40 ≤ 19 * Real.log 10 ∧ 19 * Real.log 10 < 45 := by
            refine' ⟨ _, _ ⟩;
            · norm_num [ ← Real.log_rpow, Real.le_log_iff_exp_le ];
              have := Real.exp_one_lt_d9.le ; norm_num at * ; rw [ show Real.exp 40 = ( Real.exp 1 ) ^ 40 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact le_trans ( pow_le_pow_left₀ ( by positivity ) this _ ) ( by norm_num );
            · rw [ ← Real.log_rpow, Real.log_lt_iff_lt_exp ] <;> norm_num;
              have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 45 = ( Real.exp 1 ) ^ 45 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ );
          unfold BKLNW_app.table_8_ε';
          grind ] ; norm_num;
  · -- Substitute the value of `table_8_ε'` for `b = 19 * Real.log 10`.
    have h_subst : BKLNW_app.table_8_ε' (19 * Real.log 10) = 1.93378e-8 := by
      -- Since $19 * \log 10$ is approximately $43.7$, it falls into the interval $40 \leq b < 45$, where the value is $1.93378e-8$.
      have h_interval : 40 ≤ 19 * Real.log 10 ∧ 19 * Real.log 10 < 45 := by
        refine' ⟨ _, _ ⟩;
        · norm_num [ ← Real.log_rpow, Real.le_log_iff_exp_le ];
          have := Real.exp_one_lt_d9.le ; norm_num at * ; rw [ show Real.exp 40 = ( Real.exp 1 ) ^ 40 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact le_trans ( pow_le_pow_left₀ ( by positivity ) this _ ) ( by norm_num );
        · rw [ ← Real.log_rpow, Real.log_lt_iff_lt_exp ] <;> norm_num;
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 45 = ( Real.exp 1 ) ^ 45 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ );
      unfold BKLNW_app.table_8_ε';
      grind;
    norm_num [ h_subst, Real.exp_neg, Real.exp_log ];
    ring_nf;
    unfold RS_prime.c₀; norm_num [ Real.exp_neg, Real.exp_mul, Real.exp_log ] ;
    rw [ show ( 10 : ℝ ) ^ ( 19 / 2 : ℝ ) = 10 ^ ( 9 : ℝ ) * 10 ^ ( 1 / 2 : ℝ ) by rw [ ← Real.rpow_add ] <;> norm_num, show ( 10 : ℝ ) ^ ( 38 / 3 : ℝ ) = 10 ^ ( 12 : ℝ ) * 10 ^ ( 2 / 3 : ℝ ) by rw [ ← Real.rpow_add ] <;> norm_num, show ( 10 : ℝ ) ^ ( 76 / 5 : ℝ ) = 10 ^ ( 15 : ℝ ) * 10 ^ ( 1 / 5 : ℝ ) by rw [ ← Real.rpow_add ] <;> norm_num ] ; norm_num [ ← Real.sqrt_eq_rpow ] ; ring_nf ; norm_num;
    field_simp;
    -- We'll use that $10^{2/3} \approx 4.6416$ and $10^{1/5} \approx 1.5849$ to simplify the expression.
    have h_approx : (10 : ℝ) ^ (2 / 3 : ℝ) > 4.6415 ∧ (10 : ℝ) ^ (1 / 5 : ℝ) > 1.5848 := by
      norm_num [ Real.lt_rpow_iff_log_lt ];
      exact ⟨ by rw [ div_mul_eq_mul_div, lt_div_iff₀' ] <;> norm_num [ ← Real.log_rpow, Real.log_lt_log ], by rw [ div_mul_eq_mul_div, lt_div_iff₀' ] <;> norm_num [ ← Real.log_rpow, Real.log_lt_log ] ⟩;
    nlinarith [ Real.sqrt_nonneg 10, Real.sq_sqrt ( show 0 ≤ 10 by norm_num ), mul_pos ( Real.sqrt_pos.mpr ( show 0 < 10 by norm_num ) ) ( sub_pos.mpr h_approx.1 ), mul_pos ( Real.sqrt_pos.mpr ( show 0 < 10 by norm_num ) ) ( sub_pos.mpr h_approx.2 ), mul_pos ( sub_pos.mpr h_approx.1 ) ( sub_pos.mpr h_approx.2 ) ]

/-
Check the first row of Table 14.
-/
lemma BKLNW.check_row_1 : BKLNW.check_row_prop (20, 4.2676e-5, 9.1639e-5) := by
  apply BKLNW.check_row_prop_of_simp
  · norm_num
  · rw [BKLNW_app.table_8_ε']
    norm_num
  · rw [BKLNW_app.table_8_ε']
    norm_num
    rw [RS_prime.c₀]
    norm_num
    -- We need to check: 4.2676e-5 + 1.03883 * (exp (-10) + exp (-40/3) + exp (-16)) ≤ 9.1639e-5
    -- exp(-10) ≈ 4.54e-5
    -- exp(-13.33) ≈ 1.62e-6
    -- exp(-16) ≈ 1.12e-7
    -- Sum ≈ 4.71e-5
    -- 1.03883 * 4.71e-5 ≈ 4.89e-5
    -- 4.2676e-5 + 4.89e-5 ≈ 9.1576e-5 ≤ 9.1639e-5.
    -- This is tight!
    norm_num [Real.exp_neg, Real.exp_nat_mul]
    -- We'll use the exponential property to simplify the expression. Note that $e^{16} = (e^1)^{16}$ and $e^{40/3} = (e^1)^{40/3}$.
    field_simp [Real.exp_neg];
    rw [ show ( 10 : ℝ ) = 10 by norm_num, show ( 40 / 3 : ℝ ) = 10 + 10 / 3 by norm_num, show ( 16 : ℝ ) = 10 + 6 by norm_num, Real.exp_add, Real.exp_add ] ; ring_nf;
    -- We'll use that $e \approx 2.718$ to simplify the expression.
    have h_exp : Real.exp 10 > 22026 ∧ Real.exp (10 / 3) > 28.03 ∧ Real.exp 6 > 403 := by
      refine' ⟨ _, _, _ ⟩ <;> norm_num [ Real.exp_pos ] at *;
      · have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 10 = ( Real.exp 1 ) ^ 10 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ );
      · -- We can raise both sides to the power of 3 to remove the cube root.
        have h_exp_cubed : (2803 / 100 : ℝ) ^ 3 < Real.exp (10) := by
          have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 10 = ( Real.exp 1 ) ^ 10 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_lt_of_le ( by norm_num ) ( pow_le_pow_left₀ ( by positivity ) this _ );
        contrapose! h_exp_cubed;
        exact le_trans ( by norm_num [ ← Real.exp_nat_mul ] ) ( pow_le_pow_left₀ ( by positivity ) h_exp_cubed 3 );
      · have := Real.exp_one_gt_d9.le ; norm_num at * ; rw [ show Real.exp 6 = ( Real.exp 1 ) ^ 6 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; nlinarith [ pow_le_pow_left₀ ( by positivity ) this 6 ];
    nlinarith [ mul_pos ( sub_pos.mpr h_exp.1 ) ( sub_pos.mpr h_exp.2.1 ), mul_pos ( sub_pos.mpr h_exp.1 ) ( sub_pos.mpr h_exp.2.2 ), mul_pos ( sub_pos.mpr h_exp.2.1 ) ( sub_pos.mpr h_exp.2.2 ), pow_pos ( sub_pos.mpr h_exp.1 ) 3, pow_pos ( sub_pos.mpr h_exp.2.1 ) 3, pow_pos ( sub_pos.mpr h_exp.2.2 ) 3 ]

/-
The tail of table_8 has p.1 > 25.
-/
lemma BKLNW_app.table_8_tail_gt_25 : ∀ p ∈ BKLNW_app.table_8.drop 6, 25 < p.1 := by
  simp +zetaDelta at *;
  intros a b hab;
  have h_val : ∀ p ∈ List.drop 6 BKLNW_app.table_8, 25 < p.1 := by
    simp +zetaDelta at *;
    intro a b hab;
    have h_val : ∀ p ∈ List.drop 6 BKLNW_app.table_8, 25 < p.1 := by
      simp +zetaDelta at *;
      intros a b hab
      have h_val : ∀ p ∈ List.drop 6 BKLNW_app.table_8, 25 < p.1 := by
        intro p hp
        have h_p : p ∈ List.drop 6 BKLNW_app.table_8 := hp
        have h_p : p ∈ List.drop 6 BKLNW_app.table_8 := h_p
        have h_p_val : ∀ p ∈ List.drop 6 BKLNW_app.table_8, 25 < p.1 := by
          simp +zetaDelta at *;
          intros a b hab
          have h_p_val : ∀ p ∈ List.drop 6 BKLNW_app.table_8, p.1 > 25 := by
            intro p hp
            have h_p_val : p ∈ List.drop 6 BKLNW_app.table_8 := hp
            have h_p_val : p.1 > 25 := by
              have h_p_val : ∀ p ∈ List.drop 6 BKLNW_app.table_8, p.1 > 25 := by
                exact fun p hp => by rcases p with ⟨ a, b ⟩ ; fin_cases hp <;> norm_num;
              exact h_p_val p hp
            exact h_p_val
          exact h_p_val (a, b) hab
        exact h_p_val p h_p;
      exact h_val _ hab;
    exact h_val _ hab;
  exact h_val _ hab

/-
Value of `table_8_ε` at 25.
-/
lemma BKLNW_app.table_8_ε_25_eq : BKLNW_app.table_8_ε 25 = 3.5032e-6 := by
  rw [ BKLNW_app.table_8_ε ];
  rw [ @IsGLB.csInf_eq ] <;> norm_num;
  · constructor;
    · rintro ε ⟨ a, ha, ha' ⟩ ; fin_cases ha <;> norm_num at *;
    · rintro ε hε; have := hε ⟨ _, BKLNW_app.table_8.getElem_mem ( show 5 < BKLNW_app.table_8.length by native_decide ), by norm_num ⟩ ; norm_num at * ; linarith;
  · exact ⟨ _, ⟨ _, List.mem_cons_self, by norm_num ⟩ ⟩

/-
Counterexample for row 25.
-/
lemma BKLNW.row_25_counterexample : ¬ BKLNW.check_row_prop (25, 3.5031e-6, 7.4366e-6) := by
  unfold BKLNW.check_row_prop
  intro h
  rcases h with ⟨_, hM, _⟩
  rw [BKLNW_app.table_8_ε_25_eq] at hM
  norm_num at hM

end AristotleLemmas

theorem table_14_check {b M m : ℝ} (h_table : (b, M, m) ∈ Table_14) : check_row_prop (b, M, m) := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- By definition of `check_row_prop`, we need to show that `check_row_prop (25, 3.5031e-6, 7.4366e-6)` does not hold.
  use 25, 3.5031e-6, 7.4366e-6
  simp [BKLNW.row_25_counterexample];
  -- By definition of `BKLNW.Table_14`, we know that `(25, 3.5031e-6, 7.4366e-6)` is in the table.
  simp [BKLNW.Table_14]

[Terence Tao]

OK there is an actual numerical issue here with the source table: the extended Table 8 in https://arxiv.org/src/2002.11068v2/anc/Full-Tables-Sharper-Bounds-June-2020.pdf has a worse value of $\varepsilon(25)$ (and worse precision) than the shorter Table 8 in https://arxiv.org/pdf/2002.11068. I will have to contact the authors about this.

[Terence Tao]

Just as an experiment: if one temporarily replaces the long table value 3.5032 * 10^{-6} for eps(25) in Table 8 with the slightly better short table value 3.50306 * 10^{-6}, would this restore the validity of row 25 at least?

[Terence Tao]

Hrm, according to the beginning of Appendix B: "The reported values here are displayed using a function printf which has automatically chosen to round the values. This rounding is done differently depending on the compiler used but it effects only the last digit."

In other words, it is likely that these computations were performed using nonrigorous floating point arithmetic rather than rigorous interval arithmetic. This presents a headache when it comes to formalization, especially the "top down" approach we have been pursuing in which we start from the most recent papers and follow the citations backwards. For any given numerical calculation with a roundoff issue like this, one can probably salvage the implication by adjusting the final digit of the final constant. But if we have to do this for an early reference, then the change then propagates forward through all the references, requiring a lot of small changes. Even with AI assistance, this could be rather tedious.

This is in fact making me reconsider the entire "top down" strategy, and possibly pivoting to a "bottom up" strategy where we first focus on results that do not rely heavily on previous work so as to allow for fully stable, verified numerical constants. (There is a potential third option, which is to perform top-down but only for the "static" portions of the papers in question that do not involve specific numerical values. But then we will not be able to produce any actual explicit number theory estimates for quite a long time.)

Anyway, I have contacted the authors of BKLNW in case they can offer any guidance.

[Pietro Monticone]

Aristotle negated table_8_ε.le_simp again.

The output is too long to paste here, so I put it in this gist: https://gist.github.com/pitmonticone/4a8cfd9260f97b780be6649d52d96c64.

[Pietro Monticone]

[Well, now that I think about it, I should use gists more often]

[Terence Tao]

Yeah, there is inconsistent rounding between the short and long forms of Table 8.

Perhaps what I will do as far as the project is concerned is pad the final constants in the final FKS2 paper with a safety margin, e.g., making them 0.01% worse than claimed in the paper. Then if I take the inputs at face value, this should be enough to get these slightly weaker claims. If, later on, I find that these inputs also have to be adjusted, I could give them a slightly stronger safety margin, 0.005%, and hopefully this is enough room that the derivation of the outputs to inputs remains OK. Every time I go down one level of the citation tree I will have to shrink the margin by another factor of 2, but perhaps that is good enough.

My students are aiming to develop a pipeline to automate the transfer of constants from inputs to outputs, but for the purposes of getting something formalized as a starting point, a safety margin approach may be the simplest.

[Terence Tao]

Perhaps I need to read up on safety engineering

[Terence Tao]

As an experiment: can Aristotle prove table_8_ε.le_simp if one multiplies the RHS by, say, 1.01?

[Terence Tao]

(That's an extremely generous safety margin, reaching the point where it might actually be noticeable for some applications, but could be a baseline to start from.)

[Pietro Monticone]

Terence Tao said:

As an experiment: can Aristotle prove table_8_ε.le_simp if one multiplies the RHS by, say, 1.01?

Aristotle disproved this one too https://gist.github.com/pitmonticone/7298ffe163bd6e99fc2df6364fcaf7cf.

[Terence Tao]

This one was a table data entry error (this time due to Github Copilot, rather than human error); hopefully it will now be fixed.

[Terence Tao]

I have now implemented some safety margins in the (short) Table 8 and Table 14 of BKLNW (which required some downstream methods to also incorporate such margins), and also fixed some typos coming from the transcription process from the print version of the table to Lean. I am hoping that now PNT#807 and PNT#808 can now be completed.

[Pietro Monticone]

Aristotle disproved theorem_2 as follows:

theorem theorem_2 : ∀ b ≥ 0, ∀ x ≥ exp b,
    |ψ x - x| ≤ table_8_ε b * x := by
      -- Wait, there's a mistake. We can actually prove the opposite.
      negate_state;
      -- Proof starts here:
      -- Let's choose $b = 0$.
      use 0;
      -- Let's choose $x = 1$.
      use by norm_num, 1;
      unfold BKLNW_app.table_8_ε;
      rw [ show { ε : ℝ | ∃ p ∈ BKLNW_app.table_8, p.1 ≤ 0 ∧ p.2 = ε } = ∅ by rw [ Set.eq_empty_iff_forall_notMem ] ; rintro ε ⟨ p, hp, hp', rfl ⟩ ; exact absurd hp' ( not_le_of_gt ( by fin_cases hp <;> norm_num ) ) ] ; norm_num;
      unfold ψ;
      unfold Chebyshev.psi; norm_num;

[Terence Tao]

Ah, this is because table 8 did not have any entry for b below 20 (in contrast to table 8', which had a junk value). I'll add a "junk" value of 1 at b=0 to that table which should handle these cases (e.g., using either the Chebyshev estimate or the Rosser-Schoenfeld estimate for psi). (PNT#849)

[Pietro Monticone]

Aristotle disproved theorem table_8_ε.le_simp as follows:

noncomputable section AristotleLemmas

/-
The theorem `table_8_ε.le_simp` is false because `table_8` (reference) has larger values than `table_8_ε'` (expanded) at some points, e.g. b=13000.
-/
theorem table_8_disproof : ¬ (∀ b ≥ 20, BKLNW_app.table_8_ε b ≤ BKLNW_app.table_8_ε' b) := by
  push_neg;
  -- We must show that there exists some $b \ge 20$ such that $table_8_ε' b < table_8_ε b$.
  use 25000; norm_num;
  refine' lt_of_lt_of_le _ ( le_csInf _ _ );
  rotate_left;
  exact 7.57240e-52 * 1.001 + 1e-52;
  · exact ⟨ _, ⟨ _, List.mem_cons_self, by norm_num, rfl ⟩ ⟩;
  · rintro _ ⟨ p, hp₁, hp₂, rfl ⟩ ; fin_cases hp₁ <;> norm_num at hp₂ ⊢;
  · unfold BKLNW_app.table_8_ε' ; norm_num

end AristotleLemmas

/-
**BKLNW Table 8 vs expanded Table 8**

The value of $\eps(b)$ arising from Table 8 of [reference] is weaker than that from the expanded version of Table 8 available in the arXiv.
-/
theorem table_8_ε.le_simp (b : ℝ) (hb : b ≥ 20) : table_8_ε b ≤ table_8_ε' b := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  -- By contradiction, assume there exists b ≥ 20 such that BKLNW_app.table_8_ε' b < BKLNW_app.table_8_ε b.
  by_contra h_contra;
  -- By definition of negation, if $\neg \exists b, 20 \le b \land BKLNW_app.table_8_ε' b < BKLNW_app.table_8_ε b$, then $\forall b, 20 \le b \rightarrow BKLNW_app.table_8_ε' b \geq BKLNW_app.table_8_ε b$.
  push_neg at h_contra;
  -- Apply the contradiction assumption to find the specific b where the inequality fails.
  apply table_8_disproof h_contra

[Terence Tao]

OK, that was a data transcription error: the final entry of table_8_ε' was 7.57240e-52 but on checking the source material it should have been 7.57240e-50. Hopefully that is the last of the errors!

[Steven Rossi]

Am I wrong to assume we're missing a few issues for this? FKS2 Proposition 13 mentions that the proof is basically the same as BKLNW Corollary 14.1, so I was going to do that first but can't find the ticket. Just don't want to step on any toes before finishing it

[Terence Tao]

Oh, I think you are right. Let me look at that portion of the blueprint now and see if it is in good enough shape to assign tasks for.

[Terence Tao]

OK, I have cleaned up that portion of the blueprint and issued some tasks PNT#853 PNT#854 PNT#855. The blueprint may take some time to update but once PNT#856 lands the Lean file at least should be up to date.

[Pietro Monticone]

Aristotle disproved cor_5_1_rem as follows:

theorem cor_5_1_rem (b a₂b : ℝ) (m : ℕ) (hb : (b, a₂b, m) ∈ table_cor_5_1) :
    a₂ b ∈ Set.Icc a₂b (a₂b + 10^(-m:ℝ)) := by
      -- Wait, there's a mistake. We can actually prove the opposite.
      negate_state;
      -- Proof starts here:
      -- By definition of $a₂$, we know that $a₂ 20 > 1.7$.
      use 20, 1.4263, 4
      simp [BKLNW.table_cor_5_1];
      -- By definition of $a₂$, we know that $a₂ 20 > 1.7$. Therefore, we can conclude that $1.4263 + (10^4)^{-1} < a₂ 20$.
      intro h
      have h_a2_gt : BKLNW.a₂ 20 > 1.7 := by
        -- By definition of $a₂$, we know that $a₂ 20 > 1.7$. Therefore, we can conclude that $1.4263 + (10^4)^{-1} < a₂ 20$ by using the lemma a2_20_bound.
        apply a2_20_bound
      linarith [h_a2_gt]

[Terence Tao]

Ah, you and Aristotle have picked up another typo in my formalization! I had defined $a_2$ using $f ( \lfloor b/\log 2 \rfloor + 1)$ instead of $f ( 2^{\lfloor b/\log 2 \rfloor + 1})$. These tables are turning out to be handy checksums at least. I could get an AI to check the table values separately, so hopefully with this fix it should all work out.

[Steven Rossi]

Also cor_14_1 should be theorem cor_14_1 {A B C R x₀ x : ℝ} (hx₀ : x₀ ≥ 1000)     (hEψ : Eψ.classicalBound A B C R (exp x₀)) :, i'll fix it when I get a pr in a day or two, most of the proof is done. Also I'm going to change it to let A' := (A + (R / x₀) ^ B * exp (C * sqrt (x₀ / R)) *       (a₁ x₀ * exp (-x₀ / 2) + a₂ x₀ * exp (-2 * x₀ / 3))) so that we just avoid an A != 0 hypothesis

[Steven Rossi]

Ok one more thing, to prove the antitone property of mentioned function in cor_14_1 you need B > 0. In the paper this is true, and they give a range for B for theorem 14. Should I define B to be in that range or should we keep the B > 0 hypothesis since it's a bit more general

[Steven Rossi]

Arbitrary positive B values might not hold for the general theorem, I haven't looked at it's proof yet

[Terence Tao]

Currently, Corollary 14.1 is restricting B to Set.Icc (3/2) (7/4) (which comes from (A.21) and the hypothesis $\sigma \in [0.75,1)$ in Theorem 14) which implies $B > 0$. If it turns out that you only need $B>0$ for this then you can weaken hB to strengthen the corollary without causing any harm.

[Rushil Raghavan]

Aristotle (sort of) disproved BKLNW.lem_6, in the sense that it showed that the upper bound in the hypothesis is not necessarily smaller than the upper bound in the conclusion.

Code:

lemma lem_6_counterexample_exists : ∃ c₁ c₂ c₃ c₄ k b x, 0 < c₁ ∧ 0 < c₂ ∧ 0 < c₃ ∧ 0 < c₄ ∧ 0 < k ∧
    b ≥ max (Real.log c₄) (Real.log ((4 * (c₂ + k) ^ 2) / (c₃ ^ 2))) ∧
    x ≥ Real.exp b ∧
    let A := c₁ * b ^ (c₂ + k) * Real.exp (-c₃ * Real.sqrt b)
    c₁ * (Real.log x) ^ c₂ * Real.exp (-c₃ * (Real.log x) ^ ((1:ℝ)/(2:ℝ))) > A / (Real.log x) ^ k := by
      -- Choose $c_1 = 1$, $c_2 = 1$, $c_3 = 1$, $c_4 = 1$, $k = 1$, $b = 3$.
      use 1, 1, 1, 1, 1, 3;
      refine' ⟨ Real.exp 4, _, _, _ ⟩ <;> norm_num;
      rw [ show ( 16 : ℝ ) = 2 ^ 4 by norm_num, Real.log_pow ] ; norm_num;
      refine' ⟨ _, _ ⟩;
      · exact le_trans ( mul_le_mul_of_nonneg_left ( Real.log_two_lt_d9.le ) zero_le_four ) ( by norm_num );
      · norm_num [ ← Real.sqrt_eq_rpow ];
        rw [ show ( -2 : ℝ ) = -Real.sqrt 3 + ( -2 + Real.sqrt 3 ) by ring, Real.exp_add ] ; ring_nf ; norm_num;
        rw [ mul_assoc ] ; gcongr ; nlinarith [ Real.sqrt_nonneg 3, Real.sq_sqrt ( show 0 ≤ 3 by norm_num ), Real.add_one_le_exp ( -2 + Real.sqrt 3 ) ]

It also proved the lemma under the modified hypothesis b ≥ (4 * (c₂ + k) ^ 2) / (c₃ ^ 2) instead of b ≥ log( (4 * (c₂ + k) ^ 2) / (c₃ ^ 2)). I'm not sure this is a formalization issue: in the proof of Lemma 6 here (https://arxiv.org/pdf/2002.11068), the claim "g(x) is decreasing for x ≥ (4 * (c₂ + k) ^ 2) / (c₃ ^ 2) " looks like it should be "g(x) is decreasing for log x ≥ (4 * (c₂ + k) ^ 2) / (c₃ ^ 2) ", which would be consistent with Aristotle's suggestion.

I can submit a PR with the modified hypothesis, but I'm not sure to what extent this would cause issues downstream, or if I am misunderstanding something, so I thought I should ask here first.

[Rushil Raghavan]

Also, it seems like the exponent 1/2 in PrimaryDefinitions.admissible_bound requires a typecast to the reals, I can make this change also with the PR.

[Terence Tao]

Great catch! There have been a bunch of other places where there were x vs. log x type typos. I would go ahead and make a PR with the fix (and add a comment such as the one in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/FKS2.lean#L153 or https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/FKS2.lean#L377) to note the discrepancy with the source material.

I also had to fix a number of previous issues with exponents such as 1/2 or 1/3 not being correctly typecast to Real, so please go ahead and fix these as you find them. (I wonder if there is some way to search for uses of Nat.div in general, which we would almost never use in this project I think, at least for code intended to be read by humans, as it can be so misleading.)

[Steven Rossi]

Ah i've been working on cor 14 without the latest hypothesis changes, so no assumptions on A,B,C,R. I can definitely generalize it more that the stated cases. Will have to go over the rest of the paper where those assumptions are probably necessary for the reasoning of why it's so restricted

[Terence Tao]

Oh, I put all these hypotheses in out of caution because I could not directly verify the monotonicity claim in Corollary 14.1 If they are not needed then they should simply be deleted.

[Steven Rossi]

#929 closes 14.1, will be useful in FKS2. If someone is willing to golf it in their free time I struggled a bit to make some calculations clean.

[Steven Rossi]

Got rid of all bounds on A with some restating, and loosened up B and C bounds quite a bit. We could make R less restrictive but seems fine for now.

[Pietro Monticone]

Will golf it tomorrow.