Explicit estimates, outstanding tasks v2.

Stream: PrimeNumberTheorem+

[Terence Tao]

Wow, an immense amount of progress in just over 24 hours! Thanks to all the contributors for their rapid responses, and sorry for the growing pains in rolling out the task assignment system. I would still like to transition to an issues-based system in due course, but for now we can use a more old-fashioned Zulip coordination for now.

Project 3a (showing that the least common multiple of $1,\dots,n$ is not highly abundant for large $n$) is already nearly done, with the following tasks remaining (with new Lemma numbering that should hopefully be more stable):
3a.6. Lemma 9.1.8 (Lower bound for $\sigma(M)/M$) Uses multiplicativity to verify the condition produced in Lemma 9.1.7, 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.8. Lemma 9.1.10 (choice of large primes) Uses the explicit prime number theorem of Dusart to locate primes $q_1,q_2,q_3$ with good estimates. (Formalized by @Eric Vergo )
3.a.10. Lemma 9.1.12 (Bounds for the $p_i$-product) Bounds one of the terms needed in the explicit inequality. (Formalized by @Bhavik Mehta )
3.a.11. Lemma 9.1.13 (Lower bound for the product ratio $p_i/q_i$) Bounds yet another term needed in the explicit inequality. (Formalized by @Alex Kontorovich ) MOVED to PNT#510
3.a.12. Proposition 9.1.14 (Uniform bounds for small $n$) This should be a routine arithmetic calculation. MOVED to PNT#511
3.a.14. Proposition 9.1.1 (Verification of criterion for large $n$) Verifies the criterion for $n$ large enough. MOVED to PNT#512

I will now also add the tasks of 3b (solving Erdos problem 392, which asks how efficiently one can factor $n!$ into factors of size at most $n^2$) to the queue. This is a problem which would readily follow from an unpublished claim of Erdos, but the consensus on the Erdos problem site is now that this claim was unsubstantiated. However, an alternate proof has been located, and is summarized here. Already large parts of this proof have been formalized. The proof hinges on constructing a certain approximate factorization of $n!$ that has a small "score". (The basic facts about score, and why constructing an approximate factorization with small score solved the problem, have already been formalized.) Currently, the outstanding tasks are

3.b.1. Theorem 9.2.14 (bounding the deficit of medium primes). This is a variant of Theorem 9.2.13. (Formalized by @Pietro Monticone )
3.b.2. Theorem 9.2.15 (bounding the surplus of small primes) This is similar to Theorem 9.2.13. MOVED to PNT#513
3.b.3. Theorem 9.2.16 (bounding the deficit of small primes) Similar to Theorem 9.2.14 MOVED to PNT#514
3.b.4. Theorem 9.2.17 (bounding the deficit of tiny primes) A more complicated version of Theorem 9.2.16 MOVED to PNT#515
3.b.5. Theorem 9.2.18 (bound on initial score) This is basically summing up the contributions to the score from the previous eight theorems. (Claimed by @Ruben Van de Velde )
3.b.6. Theorem 9.2.19 (showing that the initial waste is small) A simple analysis bound. (Formalized by @Pietro Monticone )
3.b.7. Theorem 9.2.20 (showing that a second contribution to the score is small) A simple application of the prime number theorem. (Formalized by @Pietro Monticone )
3.b.8. Theorem 9.2.21 (showing that a third contribution to the score is small) A crude bound. MOVED to PNT#516
3.b.9. Theorem 9.2.22 (showing that a fourth contribution to the score is small) Another application of the prime number theorem. MOVED to PNT#517
3.b.10. Theorem 9.2.23 (showing that a fifth contribution to the score is small) Yet another application of the prime number theorem. MOVED to PNT#518
3.b.11. Theorem 9.2.24 (showing that the total score is small) Combining the previous six theorems. MOVED to PNT#519

Feel free to claim any of these!

[Ruben Van de Velde]

I'll take a look at 3.b.5

[Pietro Monticone]

I would claim 3.b.1

[Bhavik Mehta]

PNT#498 does 3.a.10

[Bhavik Mehta]

I noticed the first half of Theorem 9.1.14 was also not done, that's now here: PNT#499

[Bhavik Mehta]

I think there's something missing in the combination of 9.1.15 with 9.1.12 in the proof of 9.1.1; since the $\frac{1}{n + \sqrt n}$ term appears to be claimed to be $\geq \epsilon := \frac{1}{n}$. I think it's fixable since we have slack here, but prod_epsilon_ge may need to change

[Pietro Monticone]

Params.initial.balance_small_prime_le was negated by Aristotle with $(n = 9, M = 9, L = 2, p = 2)$.

[Pietro Monticone]

Should we add M < n to the Params structure?

[Pietro Monticone]

Opened PNT#500 solving 3.b.1. Theorem 9.2.14 (bounding the deficit of medium primes).

[Terence Tao]

@Bhavik Mehta Good catch! I've opened #510 to fix this. Basically I added a third component inv_n_add_sqrt_ge to Lemma 9.1.14 (which now needs to be proven) and modified prod_epsilon_ge by adding an additional factor of $1/(1+1/89693)$ (which fortunately did not change anything in the proof, as you said there was slack in the nlinarith step).

[Pietro Monticone]

I would claim 3.b.6. Theorem 9.2.19 (showing that the initial waste is small)

[Terence Tao]

@Pietro Monticone Ah, I think the $\log n$ factors here need to be $\log n / \log 2$ (this is a crude bound for the number of powers of $p$ that can divide a number less than or equal to $n$). I'll make a PR to update this shortly (once my previous PR goes through).

[Pietro Monticone]

Oh, ok, great. Thanks!

[Terence Tao]

opened PNT#502 to insert the needed factors of $\log 2$ at various places

[Pietro Monticone]

Opened PNT#503 to solve 3.b.6. Theorem 9.2.19 (showing that the initial waste is small)

[Pietro Monticone]

I would like to claim 3.b.7.

[Bhavik Mehta]

I've done 3.a.12 and I'll claim 3.a.14

[Alex Kontorovich]

I'll claim the first unclaimed, 3.a.11.

[Alex Kontorovich]

@Pietro Monticone, should I do it "properly", that is, set up a corresponding Issue and track its progress? (Would be a good experiment for that system..

[Terence Tao]

Let me see if I can create a test issue for this problem. Give me a few mins

[Pietro Monticone]

You should already find a minimalistic task issue template "Formalisation task" that automates the addition of the issue to the dashboard ($-2 \text{ clicks } \times N_{\text{tasks}}$).

[Terence Tao]

OK I have created PNT#510. Is the process like Equational theories, in that someone just responds "claim" to claim it?

[Pietro Monticone]

Yep, see PNT#508.

[Terence Tao]

And now should I add (discussion:=510) to the Lean blueprint for this lemma?

[Pietro Monticone]

Yep

[Terence Tao]

OK. In that case I will start converting all the other outstanding tasks to issues.

[Terence Tao]

Alex, can you try officially "claiming" PNT#510 by commenting "claim" on that issue?

[Alex Kontorovich]

claimed!

[Alex Kontorovich]

Solved by AlphaProof (thanks to @Thomas Hubert for setting it up on my machine!)

[Terence Tao]

OK, now perhaps Pietro you can remind us of the workflow for linking a PR to a claimed issue

[Pietro Monticone]

Just write propose #PR_NUMBER (see PNT#508).

[Alex Kontorovich]

Cool! I see that it moved over.

[Alex Kontorovich]

So now when the PR is reviewed, it'll automatically move to "in review"?

[Alex Kontorovich]

(presumably the review has to be by someone other than me? Or I can review my own PRs?)

[Pietro Monticone]

When a reviewer approves it moves to In Review, but we can make it move at the when the issue task is liked to its solution PR for example.

[Alex Kontorovich]

I see that I can bypass merge rules and merge it immediately, but I can only "comment", not "approve" my own PR in code review :)

[Alex Kontorovich]

Pietro, can you give it a review please? :) So I can see it move along?

[Terence Tao]

I just made a review

[Alex Kontorovich]

Oh, did you want to do golfing on AI-generated proofs?

[Terence Tao]

I think it's low priority for things that don't significantly affect the typechecking time. More for aesthetics than anything else really.

[Alex Kontorovich]

Are we still in the "just let everything in if it compiles" stage, or do we want to not take on more debt, with the thought of eventually trying to get some of this into Mathlib?

[Terence Tao]

For me the main concern is total heartbeats required to typecheck the entire project. For mathlib-destined theorems of course one wants to clean up the code as much as possible, but many of the explicit estimates will not be of this form

[Alex Kontorovich]

Also, related to your other question: do we have a standard way of declaring that it was AI generated? I just added the line: "Proof found by AlphaProof"

[Terence Tao]

I'd be open to volunteers doing PRs to golf code though, even if we don't explicitly make issues for that

[Terence Tao]

I don't think we have a standard format but any sort of tagging is better than nothing, one could imagine some future AI would be more than capable of collecting a diverse set of such comments and auto-tagging code with some moderate level of accuracy

[Pietro Monticone]

Terence Tao said:

I'd be open to volunteers doing PRs to golf code though, even if we don't explicitly make issues for that

I'll make some chore: golfing sessions from time to time

[Terence Tao]

There may also be some scope for using AI tools to do some of the more routine autogolfing

[Alex Kontorovich]

Yes, that's the real dream of AI: an auto-golfer + auto-Mathlib-bound cleaner...

[Pietro Monticone]

Terence Tao said:

I don't think we have a standard format but any sort of tagging is better than nothing, one could imagine some future AI would be more than capable of collecting a diverse set of such comments and auto-tagging code with some moderate level of accuracy

Oh, we can use specific labels for that actually.

[Terence Tao]

Perhaps we could automatically record the time taken to typecheck the entire project and report it on a daily basis or something on the github? Generally I find that once a metric is posted, people will volunteer to find ways to improve it

[Pietro Monticone]

Alex Kontorovich said:

Yes, that's the real dream of AI: an auto-golfer + auto-Mathlib-bound cleaner...

Automated proof optimisation and proof repair are absolutely needed.

[Alex Kontorovich]

I don't see that the PR has moved from "In Progress" to "In Review"? Does that take some time to happen?

[Alex Kontorovich]

Maybe it won't move over before CI is done or something?

[Terence Tao]

We could create PR labels for each major tool: "Formalized using Aristotle", "Formalized using AlphaProof", etc.

[Pietro Monticone]

Terence Tao said:

We could create PR labels for each major tool: "Formalized using Aristotle", "Formalized using AlphaProof", etc.

Making them...

[Terence Tao]

OK Alex I approved your PR and it seems it automatically closed the issue.

[Pietro Monticone]

Screenshot 2026-01-10 at 00.01.15.png

[Pietro Monticone]

Let me label everything done so far

[Alex Kontorovich]

those labels go on the PR, right? Once it's merged, the PR is gone? Or do the labels go in the project itself somewhere?

[Pietro Monticone]

Those will tag the PR object

[Pietro Monticone]

Then you can filter by label and so on

[Terence Tao]

FYI, PNT#491 was proven using GPT-5 and GPT-Codex (this was not reported explicitly but communicated to me privately)

[Pietro Monticone]

Let me add the tag

[Pietro Monticone]

Screenshot 2026-01-10 at 00.05.21.png

[Alex Kontorovich]

I claimed the next one, but it looks funny?
Screenshot 2026-01-09 at 6.05.15 PM.png
why are there three theorem names attached to it?

[Terence Tao]

The three estimates here are formalized as three separate lemmas rather than having a big and statement. Two of them are already formalized, it's just the third one that needs a proof

[Pietro Monticone]

This are the aristotle PRs

[Alex Kontorovich]

Ah, I see, cool!

[Terence Tao]

By the way I'm a little confused on how the blueprint reports these multiply linked lemmas. Is it just the metadata from the last linked file that gets put into the blueprint, or the first, or some smart merging of the two? I've just duplicated the metadata for each separate linked Lean theorem but I don't know what would happen if I made the metadata different in each link.

[Terence Tao]

OK, all previous unclaimed tasks are now issues. I'll leave the previously claimed tasks grandfathered outside of the issue system to be resolved via unlinked PRs, but all new tasks going forward will use the issues system. (Alex, perhaps you could create some tasks for some other parts of the project, e.g., StrongPNT, to test out the system. I've been labeling each task with a manual tag like [LCM] to describe which subproject it is attached to.)

[Alex Kontorovich]

I just closed another one, see PNT#522

[Pietro Monticone]

Terence Tao said:

By the way I'm a little confused on how the blueprint reports these multiply linked lemmas. Is it just the metadata from the last linked file that gets put into the blueprint, or the first, or some smart merging of the two? I've just duplicated the metadata for each separate linked Lean theorem but I don't know what would happen if I made the metadata different in each link.

When multiple Lean decl link to the same blueprint decl (via the same LaTeX label), LeanArchitect performs smart merging as follows:

• \uses: combines dependencies from every linked decl
• \leanok: only appears if all linked declarations are sorry-free
• \notready: appears if any decl has notReady := true
• \mathlibok: only appears if all declarations come from mathlib
• statement, proof, title: First non-empty wins
• discussion issue number: First non-none wins

The generated LaTeX lists all declarations: \lean{a_part_one, a_part_two} of course.

In practice you can duplicate metadata across links without issue. If you change metadata between links, just be aware that titles/statements/proofs use "first wins" while dependencies merge together.

[Pietro Monticone]

Alex Kontorovich said:

I just closed another one, see PNT#522

I would avoid commenting the code that way with the new labelling system.

[Alex Kontorovich]

Alex Kontorovich said:

I just closed another one, see PNT#522

In this case, AlphaProof immediately returned a proof, but in its older version of Lean. So I had to add a few lines manually to close it, so it's proved "with AP" as opposed to "by AP" - do we want to distinguish such things?

[Pietro Monticone]

I like the approach to use the [FILE]: Title pattern. Let me change the issue template to accomodate that.

[Alex Kontorovich]

Pietro Monticone said:

Alex Kontorovich said:

I just closed another one, see PNT#522

I would avoid commenting the code that way with the new labelling system.

Got it, no need for comment

[Alex Kontorovich]

Sorry, but then if someone looks back just at the code, they won't see tags, right?

[Pietro Monticone]

Do we want to use a proper copyright/authorship comment at the beginning? Not sure...

[Alex Kontorovich]

Do you mean as if it were going into Mathlib? Won't it have 100 authors?...

[Pietro Monticone]

Yes, exactly.

[Pietro Monticone]

Leaving that comment looks ugly, doesn't it?

[Pietro Monticone]

I think people can simply filter the PRs and review the contributions there. The comment is not very effective anyway, because at this early stage we would need to keep updating it continuously to reflect ongoing changes accurately (e.g. after a golfing session).

[Pietro Monticone]

In brief, I would avoid authorship comments in the code.

[Alex Kontorovich]

I'd claimed PNT#513 (how does one refer to issues?) and sent both AlphaProof and Aristotle running on them. But my guess is it'll be too far outside the distribution for both (we'll see). How do I unclaim it, so others can try? (Have to go make dinner for the kids, and then will be swamped all weekend...)

[Pietro Monticone]

You refer in the same way PNT#513

[Pietro Monticone]

Alex Kontorovich said:

I'd claimed #513 (how does one refer to issues?) and sent both AlphaProof and Aristotle running on them. But my guess is it'll be too far outside the distribution for both (we'll see). How do I unclaim it, so others can try? (Have to go make dinner for the kids, and then will be swamped all weekend...)

Write disclaim

[Alex Kontorovich]

Ah, not unclaim.

[Alex Kontorovich]

Pietro, maybe next week we can have another session, where you teach me how to make issues?... Signing off for now

[Pietro Monticone]

Ok sure

[Pietro Monticone]

Opened PNT#523 fixing and solving 3.b.7. and fixing PNT#516, PNT#517, PNT#518 which were all misformalised in the same way (i.e. missing the P.param = param).

[Pietro Monticone]

Claimed PNT#513 and PNT#514 for Aristotle.

[Aaron Hill]

I'm unclaiming 3a.8. Lemma 9.1.10 (choice of large primes) - @Eric Vergo is going to submit a claude-code generated proof

[Pietro Monticone]

Ok, let me add the claude label

[Terence Tao]

Already did so :grinning_face_with_smiling_eyes:

[Pietro Monticone]

Ok, cool. Let me change the color to orange Claude then :joy:

[Pietro Monticone]

Added the ai label to facilitate filtering

[Harald Helfgott]

The Euler/Mittag-Leffler expansions for csc and csc^2 aren't in mathlib, right? Should I add blueprints? (The sine product formula and the expansion of cot are in fact in mathlib, it would seem.)

[Terence Tao]

Sure, that sounds like something mathlib would accept, and so worthwhile for both projects.

[Snir Broshi]

The only reciprocal trig function in Mathlib is cot, see #mathlib4 > Reciprocal trigonometric functions
Adding a result about csc might be an incentive to define csc, though sin⁻¹ isn't so bad

[(Tom de Groot) Tomodovodoo]

On a side note, I love the transition to the github issues, it feels more formal and has a nicer structure for collaboration in my opinion!

[Alex Kontorovich]

Here's a question: now that we have the issues system working, where should I add comments? Here? There? I added the following comment in PNT#566, which I guess I'll repeat here until I learn the answer:
lemma lemma_abadeulmac is mis-formalized, the integral had integrand $(\{y\}−1/2)y^{−(ℜ(s)+1)}$ but the exponent should have been $s+1$. Since that theorem wasn't quoted anywhere, I took the liberty of fixing this and also making b an integer, so it matched ZetaSum_aux2 and Zeta0EqZeta

[Terence Tao]

I think either the zulip or the PR is a good forum; the zulip will get broader visibility so I guess it comes down to whether you just want to clarify with the person originating the PR (in this case, me) or whether you want to involve all the other participants as well.

[Alex Kontorovich]

Ok, this is done. I had to change the statement a bit to make it true (missing a term). I didn't check how this propagates (in the TeX) through the rest of the blueprint. See PNT#578.

[Alex Kontorovich]

Shoot, I'm only now seeing @Pietro Monticone's message in github that there was a clash with @Bhavik Mehta's work? Argh.

[Alex Kontorovich]

Oh wait, that's ... for a different issue? I'm so confused...

[Alex Kontorovich]

I see, that was for the smaller goal, not this zeta goal.

[Pietro Monticone]

Your PR seems to make changes both in Lcm and ZetaAppendix. Can I fix the merge conflict?

[Alex Kontorovich]

I merged to resolve the conflict and keep Bhavik's proof

[Pietro Monticone]

Oh, ok. Cool.

[Terence Tao]

Hmm, I may need @Harald Helfgott to weigh in on this. Using the blueprint https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/zeta-chapter.html#a0000000031 as reference, Alex are you saying that Lemma 7.4.7 does not seem to be true as stated, and one needs to make $b$ an integer rather than a half-integer (and add half of the final term to the RHS)? This would indeed necessitate several changes to downstream lemmas, so if there is an alternate fix that can somehow fit with the spirit of the original wording of 7.4.7 this may be preferable.

[Pietro Monticone]

We might want to use a common syntax for PR titles so that it's immediately clear from the get go (e..g notification or first look at the list of issues) what has been changed and where.

[Alex Kontorovich]

Well, I was trying to be lazy and quote the theorem that we'd already proved in PNT (namely,  Lemma 3.4.4), but that's for integer values of b and has an extra term

[Pietro Monticone]

I'm applying the Mathlib conventions in my PRs. I think they work nicely.

[Terence Tao]

OK... so the half-integer version might still be true? It might be derivable from the integer version, if $b = k +1/2$ one needs to prove something like $s \int_k^b (\{y\}-1/2) \frac{dy}{y^{s+1}} = -\frac{k^{1-s}}{1-s} + \frac{b^{1-s}}{1-s} + \frac{1}{2b^s}$ which should just be some fundamental theorem of calculus calculation.

[Terence Tao]

(debating whether to check my calculation using pen and paper or a LLM. What the heck, let's try an LLM). EDIT: ChatGPT has corrected me to $s \int_k^b (\{y\}-1/2) \frac{dy}{y^{s+1}} = -\frac{k^{1-s}}{1-s} + \frac{b^{1-s}}{1-s} + \frac{1}{2k^s}$, which in retrospect makes sense and should be provable by an integration by parts (or a further appeal to Euler-Maclaurin).

[Alex Kontorovich]

yes, sorry, by "not true", I meant, not true if b is made an integer.

[Alex Kontorovich]

maybe we can make what i did lemma_abadeulmac' and put back the original lemma_abadeulmac. Then it's an easy calculation to go from the former to the latter.

[Terence Tao]

Two lemmas are better than one. I can imagine some applications will have a slight preference for the integer version rather than the half-integer one.

[Alex Kontorovich]

Great, I'll do it. This would be a good excuse for me to ask @Pietro Monticone to teach me how to use the issues system... :)

[Terence Tao]

OK, so PNT#578 is still a work in progress because the lemma_abadeulmac' to lemma_abadeulmac conversion is not yet formalized?

[Alex Kontorovich]

Ok the original lemma_abadeulmac is now proved (and fixed, with complex exponent on y). I ended up using AlphaProof to solve it. Annoyingly, the Lean/Mathlib versions were significantly different that it took quite a bit of massaging from its solution to the one that's there. But it's done, and b is back to being a half-integer.

[Alex Kontorovich]

Oh darn, that ruins my chance to make a new Issue myself. Oh well, I'm sure I'll find another opportunity. (FYI I'm traveling to Boston tomorrow, so will not have as much time for the next few days.)

[Harald Helfgott]

Terence Tao said:

Hmm, I may need Harald Helfgott to weigh in on this. Using the blueprint https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/zeta-chapter.html#a0000000031 as reference, Alex are you saying that Lemma 7.4.7 does not seem to be true as stated, and one needs to make $b$ an integer rather than a half-integer (and add half of the final term to the RHS)? This would indeed necessitate several changes to downstream lemmas, so if there is an alternate fix that can somehow fit with the spirit of the original wording of 7.4.7 this may be preferable.

The statement for half-integers in my TeX/PDF is correct. There seems to have been a misunderstanding while I was asleep (different timezone!) but this appears to have resolved itself.

There now seem to be two statements in the blueprint: one for $b$ an integer and one for $b$ a half-integer. Due to a multiply-defined label issue, I cannot currently see the latter statement, so I cannot check whether it has been changed. Whatever has been done to it, if anything, I presume it is still a correct statement, since it has been proved :).

Using half-integers in this and related contexts, while possibly not customary, is completely natural, in the same way that the midpoint method in integration is "better" than the left or right triangle rule.

I'd be in favor of having one version of the lemma for b a half-integer (it's not just natural but a bit simpler) and another one for completely arbitrary real b.

[Harald Helfgott]

@Alex Kontorovich said:

maybe we can make what i did lemma_abadeulmac' and put back the original lemma_abadeulmac. Then it's an easy calculation to go from the former to the latter.

In light of what I just said - proving the case of $b$ an integer and deducing the case of $b$ a half-integer from it goes in the backward direction. (I don't want to nitpick, but it is best to set some standards in a trivial case that is easy to resolve.)

Conceptually, it seems cleaner to either

• prove the case of $b$ a half-integer from scratch, and the case of $b$ real separately, or
• prove the case of $b$ real first, and either just apply it, or have the case of $b$ a half-integer as a corollary -- a term just drops out.

I'd go with whichever of these two options is simplest from the point of view of Lean.

[Harald Helfgott]

(deleted)

[Pietro Monticone]

lemma_abadeuleulmit1 was negated by Aristotle:

theorem lemma_abadeuleulmit1 {z : ℂ} (hz : ¬∃ n : ℤ, z = n) :
    (π / Complex.sin (π * z) : ℂ) =
      (1 / z : ℂ) + ∑' n : ℤ, (-1) ^ n * ((1 / (z - n) : ℂ) + (1 / (z + n) : ℂ))

In particular:

/- Disproof of the user's theorem. -/
lemma lemma_abadeuleulmit1_disproof :
  ¬ (∀ z : ℂ, (¬∃ n : ℤ, z = n) →
    (π / Complex.sin (π * z) = 1 / z + ∑' n : ℤ, (-1 : ℂ) ^ n * (1 / (z - n) + 1 / (z + n)))) := by
      -- Assume there exists such a $z$ for which the statement is true.
      by_contra h_contra;
      -- Apply the assumption to $z = 1/2$.
      specialize h_contra (1 / 2);
      rw [ show ( ∑' n : ℤ, ( -1 : ℂ ) ^ n * ( 1 / ( 1 / 2 - n ) + 1 / ( 1 / 2 + n ) ) ) = 2 / ( 1 / 2 : ℂ ) + 2 * ∑' n : ℕ+, ( -1 : ℂ ) ^ ( n : ℤ ) * ( 1 / ( 1 / 2 - n ) + 1 / ( 1 / 2 + n ) ) from ?_ ] at h_contra;
      · rw [ show ( ∑' n : ℕ+, ( -1 : ℂ ) ^ ( n : ℤ ) * ( 1 / ( 1 / 2 - n ) + 1 / ( 1 / 2 + n ) ) ) = ( Real.pi / Complex.sin ( Real.pi * ( 1 / 2 ) ) ) - 1 / ( 1 / 2 : ℂ ) by
              rw [ lemma_correct_expansion ] ; norm_num [ mul_div ];
              rintro ⟨ _ | n ⟩ <;> norm_num [ Complex.ext_iff ] <;> linarith ] at h_contra ; norm_num [ Complex.ext_iff, Real.pi_ne_zero ] at h_contra;
        norm_num [ mul_div ] at h_contra;
        linarith [ Real.pi_gt_three, h_contra fun x => by rcases x with ⟨ _ | _ | x ⟩ <;> norm_num <;> linarith ];
      · convert lemma_sum_Z_split _ _ using 1;
        rintro ⟨ _ | n ⟩ <;> norm_num [ Complex.ext_iff ] <;> linarith

[Harald Helfgott]

@Pietro Monticone Oh. I think it's just that I always use $\sum_n$ to mean $\sum_{n>0}$ (as I made clear in a "notation" paragraph) and this seems to have been translated as $\sum_{n\ne 0}$ instead.

[Alex Kontorovich]

Harald Helfgott said:

In light of what I just said - proving the case of $b$ an integer and deducing the case of $b$ a half-integer from it goes in the backward direction. (I don't want to nitpick, but it is best to set some standards in a trivial case that is easy to resolve.)

We already had a proof for $b$ a natural number, but stated slightly differently. So all I had to do was connect the existing proof to the statement being claimed. From there it was easy to deduce the half-integer (and in fact, any real) version. We can include a version for all reals if we really want to, it's no harder than what's done already. But if it's not needed for the current application, I guess I would only do it when it's time to upstream to Mathlib...

[Harald Helfgott]

For arbitrary order, starting from the real version (not from the version with $b$ an integer) is clearly the right way to go.

[Alex Kontorovich]

Pietro Monticone said:

lemma_abadeuleulmit1 was negated by Aristotle:

The statement is fixed in PNT#587 (waiting for the last merge to compile before merging this)

[Notification Bot]

13 messages were moved from this topic to #PrimeNumberTheorem+ > CI issues by David Renshaw.

[Pietro Monticone]

Ok, just wrapped up a 2-hour call with @Harald Helfgott presenting a tutorial covering:

• VS Code basics
• GitHub workflow
• GitHub integration within VS Code
• Aristotle usage

He shared two documents:

• ZetaAppendix_blueprint.tex (6 pages)
• ZetaAppendix_paper.tex (2 pages).

We've submitted both to Aristotle for autoformalisation. Let's see how it goes.

[Harald Helfgott]

Many thanks, Pietro! Right, the 2-page file contains the original, pre-blueprint version of the appendix, meant for humans. (Perhaps it was a little terse at places, even for humans.) Let us see how far Aristotle manages to munch through it.

[Pietro Monticone]

Regarding granularity, task PNT#548 (solved by PR PNT#591) proved a bit coarse for Aristotle (roughly measured by the number of necessary auxiliary lemmas or total auxiliary lines of code). That said, granularity likely depends heavily on mathlib-adjacency, which makes it non-trivial to calibrate in advance.

[Terence Tao]

As a very broad rule of thumb, Lean + Mathlib fares somewhat better with purely algebraic calculations (e.g., symbolically differentiating a complicated expression) than with analytic tasks, such as checking that the integration by parts formula continues to hold when one term is of bounded variation and the other is continuous. Steps that are easy for human analysts ("by the usual limiting argument, we may assume that f is smooth and compactly supported") can be unexpectedly difficult for Lean, even with the autoformalization tools. I guess we will get more data on this as we continue this project.

[Harald Helfgott]

@Terence Tao I expected as much - but it is a mystery to me as to which analytic step here was found by Lean to be "not algebraic". What exactly did Aristotle find difficult, or had to greatly expand?

[Terence Tao]

You can see what Aristotle did at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/591/files . For instance, it used the Bernstein polynomial approximator to approximate continuous functions by smooth (polynomial) functions, then spent considerable effort showing that the Bernstein approximation of a monotone function was still monotone. This is probably not the route a human formalizer would have taken, but it (eventually) worked.

[Harald Helfgott]

Let me try to read this. (Woke up in the middle of the night...)

In lemma_aachmonophase itself, what the formalizer has filled in is the sort of small steps that we point at but don't write down, yet a calculus student usually would: $h(t) e(\phi(t)) = (h(t)/\phi'(t)) (\phi'(t) e(\phi(t))) = (h(t)/\phi'(t))\cdot \frac{1}{2\pi i} \frac{d e(\phi(t))}{dt}$. So far, so normal. The real action happens in lemma_IBP_bound_abs_antitone, which proves that $\left|\int_a^b g(t) F'(t)\right|\leq \max |F(t)| \cdot 2 |g(a)|$ for $g:[a,b]\to \mathbb{R}$ continuous with $|g(t)|$ non-decreasing, and $F:[a,b]\to \mathbb{C}$ in $C^1$ (I think). I like this reduction, by the way: nice and pedagogical.

Now let us look at lemma_IBP_bound_abs_antitone. Let me not yet hazard a guess as to what goes awry...

[Harald Helfgott]

At this point, things are evident to a human being, particularly upon being told that you proceed by integration by parts: $\int_a^b g(t) F'(t) = g(b) F(b) - g(a) F(a) - \int_a^b F(t) dg(t)$; now, $|g(b) F(b)-g(a) F(a)|\leq (|g(b)|+|g(a)|) \max |F(t)|$, and $\left|\int_a^b F(t) dg(t)\right| \leq \max |F(t)|\cdot \int_a^b |dg(t)|\leq \max |F(t)|\cdot (|g(b)|-|g(a)|)$. Let us see where the formalizer tripped, in spite of having a proof for humans in front of it.

[Harald Helfgott]

The second half of the proof of lemma_IBP_bound_abs_antitone consists, indeed, of the algebra in the above, done prolixly; in fact, it's doing things twice, depending on whether $g(t)$ is non-negative or non-positive throughout $[a,b]$. The first half is spent proving that we are in one of these two cases. That's funny - you don't need to prove that, as that argument is already carried out inside Lemma lemma_aachra. At any rate, the AI manages to do that on its own. (Naïve question: did it learn something from the proof of Lemma lemma_aachra, or is that outside the context as far as it's concerned?) I take it doesn't find arguments by IVT to be difficult; good.

[Harald Helfgott]

(deleted)

[Harald Helfgott]

So, now it just has to prove that $\left|\int_a^b F(t) dg(t)\right|\leq \max |F(t)|\cdot (g(b)-g(a))$ for $g$ continuous and monotone (monotone? it must mean increasing) and $F$ in $C^1$ (of course bounded would be enough). That is theorem lemma_IBP_bound_monotone. I wonder what can go wrong.

[Harald Helfgott]

Notice how it's actually still writing $\int_a^b F'(t) g(t) dt - \left. F(t) g(t)\right|_a^b$ instead of $\int_a^b F(t) dg(t)$. I think we can all see where things are going now: Lean/Mathlib may be deeply uncomfortable with really basic, colloquial measure theory. Or Aristotle is.

[Harald Helfgott]

So uncomfortable, in fact, that it won't use Lemma lemma_aachra at all; it can't reduce to it.

[Harald Helfgott]

This is the point at which Aristotle gets lost in the forest (and yet somehow manages to find a way out of it, in the end, after being unnecessarily cold and hungry). I think I'll try to get some more sleep and let others take over from here. I repeat: we've been reading backwards and, so far, nothing has been so surprising. What remains (and this is what takes 370 lines) is to prove that $\left|\int_a^b F'(t) g(t) dt - \left. F(t) g(t)\right|_a^b\right|\leq \max |F(t)[\cdot (g(b)-g(a))$ for $g$ continuous and non-decreasing, and $F$ in $C^1$. What we need to understand is why Aristotle finds this hard. (Can this really not be expressed in Lean/Mathlib in a very straightforward way due to a gap in the library? Or perhaps that was the case in an earlier version of Mathlib that Aristotle was trained on?)

[Lawrence Wu (llllvvuu)]

It might have had trouble writing F(t)g’(t) because it didn’t assume g to be differentiable. I don’t know if that’s a real mathematical obstruction, but I can see how an AI would get bogged down by such details if it’s not considering the big picture.

[Harald Helfgott]

Exactly, that's part of the matter, and also why I'm writing $dg(t)$ instead of $g'(t)$. It's something we know to be a non-issue, but a very scrupulous Calculus student would have doubts.

[Harald Helfgott]

I'd first want to know whether this is an Aristotle issue or a Mathlib issue. Can a human easily formalize the following?
(a) integration by parts: $$\int_a^b F'(t) g(t) dt - F(t) g(t)\right|_a^b = - \int_a^b F(t) dg(t)$$ for $F$ in $C^1$ and $g$ of bounded variation,

(b) $\left|\int_a^b F(t) dg(t) \right|\leq \max |F(t)|\cdot (g(b)-g(a))$ for $F$ in $C^1$ and $g$ increasing.

Note that, by this point, you can drop the assumption that $g$ is continuous. (To be a bit pedantic, you don't actually need $F$ to be $C^1$ either; AC is enough.)

I thought (a) was in Mathlib as-is? Can't find it right now.

[Sébastien Gouëzel]

We don't have in Mathlib the signed measure $dg$ when $g$ is of bounded variation. What we have is the Stieltjes measure associated to a right-continuous monotone function, and that a function of bounded variation is the difference of two monotone functions, so it wouldn't be hard to build, but it's not there. Which means that Aristotle can't use it, of course!

[Lawrence Wu (llllvvuu)]

In this case, g is a continuous monotone function, but only on [a, b], which may make it challenging to use docs#StieltjesFunction. I guess it is not easy to come up with an API that avoids subtypes.

[Lawrence Wu (llllvvuu)]

I guess that Aristotle either didn't consider docs#StieltjesFunction at all, or decided it would be easier to just get a C1 approximation to g, which explains the additional 370 lines

[Yongxi Lin (Aaron)]

Lawrence Wu (llllvvuu) said:

In this case, g is a continuous monotone function, but only on [a, b], which may make it challenging to use docs#StieltjesFunction. I guess it is not easy to come up with an API that avoids subtypes.

This shouldn't be challenging right? StieltjesFunction.measure has already been generalized to a large class of linearly ordered set.

[Thomas Zhu]

Could be because that generalization happened only a month ago but Aristotle runs on v4.24.0?

[Sébastien Gouëzel]

Even if Aristotle were on current Mathlib, I don't think it could make the link from what we currently have to signed measures for bounded variation functions, because that's API building and it's not where it shines most. But I agree that there's nothing mathematically challening to do here given what we have: it's just API building, but it has to be done by someone (and the correct API is not obvious, as far as I can tell, because there are subtleties between open/closed/semiinfinite intervals and the handling of boundary points).

[Harald Helfgott]

Well, I am glad that a lemma I innocently proposed for (auto)formalization has highlighted a gap that matters for many things and ought to be filled.

Let us also think ahead. As I said in a different thread (#PrimeNumberTheorem+ > Euler-Maclaurin, Poisson summation), we will have to think of what framework we want to set to ensure decay of Fourier transforms, arbitrary-order Euler-Maclaurin, etc. "Be in the Sobolev space you'd expect" is often a stronger condition that needed, and it isn't fulfilled in many applications.

(A simple example: consider the triangle function. Shouldn't you be able to tell its Fourier transform has $\ll 1/t^2$ decay as $t\mapsto \pm \infty$, without computing it?)

One reasonable kind of condition I mentioned in the other thread would be "Let $f\in L^1$ be such that the $$k$$th distributional derivative $D^k$ is a finite signed measure". However, if we don't have signed measures there, and won't have them right away, we'll have to use something else, or at least word it a bit differently.

Let us focus on $k=2$, since that may be the most common case: $\ll 1/t^2$ decay is enough for the Fourier transform to be integrable. Then one option (equivalent to the above for $k=2$, I'd think) would be to say: "Let $f\in L^1$ be absolutely continuous. Assume there exists a function $g$ of finite total variation on $\mathbb{R}$ such that $g=f'$ a.e." We could also require $g$ to be right-continuous (say) if we want it to be unique.

Thoughts?

[Harald Helfgott]

On a related note --

Pietro Monticone said:

Ok, just wrapped up a 2-hour call with Harald Helfgott presenting a tutorial covering:

• VS Code basics
• GitHub workflow
• GitHub integration within VS Code
• Aristotle usage

He shared two documents:

• ZetaAppendix_blueprint.tex (6 pages)
• ZetaAppendix_paper.tex (2 pages).

We've submitted both to Aristotle for autoformalisation. Let's see how it goes.

I'm afraid it didn't get that far on blueprint.tex, at least not on the version I submitted. It seems to have tied itself in knots very early over the issue of integration by parts, though not necessarily in the same way that it tied itself in knots over the same issue when we fed it the blueprint piecemeal (and when we or rather you did that, it actually found a way out, though a rather roundabout one, as we have just discussed).

[Pietro Monticone]

I’m running the third iteration. In the second it started formalising the first lemma. Let’s see how it goes.

[Pietro Monticone]

I submitted this prompt by @Harald Helfgott to Aristotle:

Let $F : [a,b] \to \mathbb{C}$ be in $C^1([a,b])$.

(a) Integration by parts:
\[
  \int_a^b F'(t) g(t) \, dt - \left. F(t) g(t) \right|_a^b = - \int_a^b F(t) \, dg(t)
\]
for $g : [a,b] \to \mathbb{R}$ of bounded variation.

(b) For $F$ in $C^1$ and $g : [a,b] \to \mathbb{R}$ increasing:
\[
  \left| \int_a^b F(t) \, dg(t) \right| \leq \max |F(t)| \cdot (g(b) - g(a)).
\]

Aristotle autoformalised it as follows (IBP_bound.lean):

-- ...

/-
Integration by parts formula for Stieltjes integral.
-/
theorem stieltjes_integration_by_parts
  (g : StieltjesFunction)
  (F : ℝ → ℂ)
  (a b : ℝ)
  (hab : a ≤ b)
  (hF : ContDiffOn ℝ 1 F (Set.Icc a b)) :
  ∫ t in a..b, deriv F t * (g t : ℂ) = F b * g b - F a * g a - stieltjesIntegral g F a b := by
    have := @stieltjes_ibp_intermediate g F a b hab hF;
    have := @stieltjes_ibp_lhs_expansion g F a b hab ( hF.continuousOn );
    grind

/-
Bound for the Stieltjes integral.
-/
theorem stieltjes_integral_bound
  (g : StieltjesFunction)
  (F : ℝ → ℂ)
  (a b M : ℝ)
  (hab : a ≤ b)
  (hF : ContinuousOn F (Set.Icc a b))
  (hM : ∀ t ∈ Set.Icc a b, ‖F t‖ ≤ M) :
  ‖stieltjesIntegral g F a b‖ ≤ M * (g b - g a) := by
    -- We'll use the fact that |F| ≤ M to bound the integral.
    have h_integral_le : ‖stieltjesIntegral g F a b‖ ≤ ∫ x in a..b, ‖F x‖ ∂g.measure := by
      convert MeasureTheory.norm_integral_le_integral_norm _ using 1;
      rotate_left;
      rw [ intervalIntegral.integral_of_le hab ];
      exacts [ by infer_instance, by rw [ stieltjesIntegral ] ; rw [ intervalIntegral.integral_of_le hab ] ];
    refine' le_trans h_integral_le _;
    rw [ intervalIntegral.integral_of_le hab ];
    refine' le_trans ( MeasureTheory.integral_mono_of_nonneg _ _ _ ) _;
    refine' fun x => M;
    · exact Filter.Eventually.of_forall fun x => norm_nonneg _;
    · norm_num [ MeasureTheory.integrable_const_iff ];
      exact Or.inr ⟨ by simp +decide [ hab ] ⟩;
    · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Ioc ] with x hx using hM x <| Set.Ioc_subset_Icc_self hx;
    · simp +decide [ mul_comm, hab ];
      rw [ MeasureTheory.measureReal_def, g.measure_Ioc ];
      rw [ ENNReal.toReal_ofReal ( sub_nonneg.mpr <| mod_cast g.mono hab ) ]

[Alex Kontorovich]

Such things should get upstreamed directly, no? With some more API around them? What do you think @Sébastien Gouëzel?

[Sébastien Gouëzel]

stieltjesIntegral is not defined in Mathlib, so I guess it's something Aristotle defines earlier in the file -- if it's just the integral wrt g.measure, I doubt it's worth introducing a specific notion? It probably shouldn't be upstreamed like that, because the generality is not good (F should take values in an arbitrary normed space, for instance, and also it's assuming that g is globally a Stieltjes function while what should matter is only the behavior on [a, b]).

The "correct" statement should assume that g is a bounded variation function on [a,b] (taking values in some Banach space), associate to it the vector measure dg (which we don't have in Mathlib, and which can't be built straight away using Stieltjes measures because there is no order structure in the target space), and then show for any continuous bilinear map L a formula like ∫ t in a..b, L (deriv F t) (g t) = vector integral of F wrt the measure dg and L. Except that we don't have the integral wrt vector measures yet (although there is a sequence of PRs leading there). We will get there, but not nearly as quickly as in a side project like PNT.

[Alex Kontorovich]

Got it, thanks!

[Sébastien Gouëzel]

Note that for many practical uses the theorem above is already great, and I'm amazed by Aristotle's abilities!

[Pietro Monticone]

I've attached the full output above.

[Pietro Monticone]

Yes, this is the definition of stieltjesIntegral introduced by Aristotle at the beginning of the file:

/-
Definition of the Riemann-Stieltjes integral for a Stieltjes function (monotone right-continuous).
-/
def stieltjesIntegral (g : StieltjesFunction) (F : ℝ → ℂ) (a b : ℝ) : ℂ :=
  ∫ x in a..b, F x ∂g.measure

[Harald Helfgott]

I was about to say that I am impressed. What is the definition of StieltjesFunction? Is it part of Mathlib?

@Sebastien Gouzel I imagine that, for the while being, we can do what was done historically, and what is often done pedagogically: start with the Riemann-Stieltjes integral. It seems Aristotle has done exactly that - but how? I imagine it must have a definition in the literature in its database, no?

[Sébastien Gouëzel]

Thinking again about it, stieltjes_integration_by_parts would probably already be a good fit for Mathlib today (without introducing the definition stieltjesIntegral and taking a function F with values in a general Banach space) because it won't be superseded by the general theorem I'm thinking of (which would be for integrals wrt vector measures instead of usual measures).

[Harald Helfgott]

Well, we can start with RiemannStieltjesIntegral, and plan for LebesgueStieltjesIntegral.

[Sébastien Gouëzel]

StieltjesFunction is part of Mathlib (monotone cadlag functions), and the hard mathematical part (constructing the measure dg) is already in Mathlib also.

[Harald Helfgott]

Ah, good.

[Terence Tao]

There may be some synergy here with PNT#598 PNT#599, which starts proving some identities in the paper of Rosser and Schoenfeld (e.g., $\pi(x) = \frac{\vartheta(x)}{\log x} + \int_2^x \frac{\vartheta(y)\ dy}{y \log^2 y}$) by setting up a Stieltjes integral using the StieltjesFunction machinery in Mathilb. (Most likely these identities also appear prior to the Rosser-Schoenfeld paper, but I do not have an earlier reference available.)

[Lawrence Wu (llllvvuu)]

How ergonomic is it to use docs#StieltjesFunction for docs#MonotoneOn functions? The naive ways I can think of would be to replace the tails with constant functions, or to mess with subtypes. Am I missing a cleaner way? Or would it also be useful to have some kind of StieltjesFunctionOn (based on docs#BoundedVariationOn)

[Pietro Monticone]

Sébastien Gouëzel said:

stieltjesIntegral is not defined in Mathlib, so I guess it's something Aristotle defines earlier in the file -- if it's just the integral wrt g.measure, I doubt it's worth introducing a specific notion? It probably shouldn't be upstreamed like that, because the generality is not good (F should take values in an arbitrary normed space, for instance, and also it's assuming that g is globally a Stieltjes function while what should matter is only the behavior on [a, b]).

The "correct" statement should assume that g is a bounded variation function on [a,b] (taking values in some Banach space), associate to it the vector measure dg (which we don't have in Mathlib, and which can't be built straight away using Stieltjes measures because there is no order structure in the target space), and then show for any continuous bilinear map L a formula like ∫ t in a..b, L (deriv F t) (g t) = vector integral of F wrt the measure dg and L. Except that we don't have the integral wrt vector measures yet (although there is a sequence of PRs leading there). We will get there, but not nearly as quickly as in a side project like PNT.

Out of curiosity, I basically gave this as a prompt to Aristotle and it started with:

/-
Defines the vector integral of a simple function with respect to a vector measure and a bilinear map.
-/
open MeasureTheory Set Filter Topology

def MeasureTheory.SimpleFunc.vectorIntegral {α F G H : Type*} [MeasurableSpace α]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    [NormedAddCommGroup H] [NormedSpace ℝ H]
    (μ : VectorMeasure α G) (L : F →L[ℝ] G →L[ℝ] H) (s : SimpleFunc α F) : H :=
  s.range.sum fun x => L x (μ (s⁻¹' {x}))

theorem MeasureTheory.SimpleFunc.vectorIntegral_const {α F G H : Type*} [MeasurableSpace α]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    [NormedAddCommGroup H] [NormedSpace ℝ H]
    (μ : VectorMeasure α G) (L : F →L[ℝ] G →L[ℝ] H) (c : F) :
    MeasureTheory.SimpleFunc.vectorIntegral μ L (SimpleFunc.const α c) = L c (μ univ) := by
      proof -- not reporting for brevity.

-- [...]

/-
A vector measure μ is a Stieltjes vector measure for g if μ((a, b]) = g(b+) - g(a+) for all a ≤ b.
-/
open MeasureTheory Set Filter Topology

/-- `IsStieltjesVectorMeasure g μ` means that `μ` is the Stieltjes measure associated to `g`.
    Specifically, for any interval `(a, b]`, `μ (Ioc a b) = g(b+) - g(a+)`. -/
def IsStieltjesVectorMeasure {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (g : ℝ → E) (μ : VectorMeasure ℝ E) : Prop :=
  ∀ a b, a ≤ b → μ (Ioc a b) = Function.rightLim g b - Function.rightLim g a

/-
Defines stieltjesVectorMeasure g as the vector measure associated to g if it exists, otherwise 0.
Proves that if such a measure exists, stieltjesVectorMeasure g satisfies the Stieltjes property.
-/
open MeasureTheory Set Filter Topology

noncomputable def stieltjesVectorMeasure {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (g : ℝ → E) : VectorMeasure ℝ E :=
  if h : ∃ μ : VectorMeasure ℝ E, IsStieltjesVectorMeasure g μ then Classical.choose h else 0

/-
Defines Integrable f as the existence of a sequence of simple functions converging to f pointwise such that their integrals form a Cauchy sequence.
Defines vectorIntegral f as the limit of the integrals of such a sequence.
-/
open MeasureTheory Set Filter Topology

def Integrable {α F G H : Type*} [MeasurableSpace α]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    [NormedAddCommGroup H] [NormedSpace ℝ H]
    (μ : VectorMeasure α G) (L : F →L[ℝ] G →L[ℝ] H) (f : α → F) : Prop :=
  ∃ s : ℕ → SimpleFunc α F,
    (∀ x, Tendsto (fun n => s n x) atTop (nhds (f x))) ∧
    CauchySeq (fun n => MeasureTheory.SimpleFunc.vectorIntegral μ L (s n))

noncomputable def vectorIntegral {α F G H : Type*} [MeasurableSpace α]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]
    (μ : VectorMeasure α G) (L : F →L[ℝ] G →L[ℝ] H) (f : α → F) : H :=
  if h : Integrable μ L f then
    lim (atTop.map (fun n => MeasureTheory.SimpleFunc.vectorIntegral μ L (Classical.choose h n)))
  else 0

/-
Summation by parts formula for bilinear maps.
sum (f(i+1) - f(i)) g(i) = f(n)g(n) - f(0)g(0) - sum f(i+1) (g(i+1) - g(i)).
-/
open MeasureTheory Set Filter Topology

variable {E F H : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [NormedAddCommGroup H] [NormedSpace ℝ H]

theorem summation_by_parts_vector
    (L : F →L[ℝ] E →L[ℝ] H)
    (f : ℕ → F) (g : ℕ → E) (n : ℕ) :
    (∑ i ∈ Finset.range n, L (f (i + 1) - f i) (g i)) =
    L (f n) (g n) - L (f 0) (g 0) -
    ∑ i ∈ Finset.range n, L (f (i + 1)) (g (i + 1) - g i) := by
      proof -- not reporting for brevity

--- [...]

/-
Defines the Riemann-Stieltjes vector integral as the limit of Riemann sums.
-/
open MeasureTheory Set Filter Topology

variable {E F H : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
  [NormedAddCommGroup H] [NormedSpace ℝ H] [CompleteSpace H]

noncomputable def vectorIntegralRS (μ : VectorMeasure ℝ E) (L : F →L[ℝ] E →L[ℝ] H) (f : ℝ → F) (a b : ℝ) : H :=
  lim (map (fun (P : TaggedPartition a b) => vectorRiemannSum μ L f P) (comap TaggedPartition.mesh (nhds 0)))

Submitted the second run on the same prompt.

[Pietro Monticone]

The following declarations were negated by Aristotle:

theorem eq_413 {f : ℝ → ℝ} (hf : DifferentiableOn ℝ f (Set.Ici 2)) (x : ℝ) :
    ∑ p ∈ Finset.filter Nat.Prime (Finset.range ⌊x⌋₊), f p =
      f x * θ x / log x -
      ∫ y in 2..x, θ y * deriv (fun t ↦ f t / log t) y

theorem eq_418 (x : ℝ) :
    ∑ p ∈ Finset.filter Nat.Prime (Finset.range ⌊x⌋₊), 1 / p =
      θ x / (x * log x) +
      ∫ y in 2..x, θ y * (1 + log y) / (y ^ 2 * log y ^ 2)

[Bhavik Mehta]

I'm guessing x >= 2 is intended for both of these

[Pietro Monticone]

Yep, fixing those.

[Pietro Monticone]

(deleted)

[Terence Tao]

Actually the issue is that Finset.range ⌊x⌋₊ should be Finset.Iic ⌊x⌋₊ or Finset.Ioc 0 ⌊x⌋₊. Sorry for the misformalization

[Pietro Monticone]

Yes, I'm changing it with:

theorem eq_413 {f : ℝ → ℝ} (hf : DifferentiableOn ℝ f (Set.Ici 2)) {x : ℝ} (hx : 2 ≤ x) :
    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), f p = f x * θ x / log x -
      ∫ y in 2..x, θ y * deriv (fun t ↦ f t / log t) y := by
  sorry

[Pietro Monticone]

and obviously:

theorem eq_418 {x : ℝ} (hx : 2 ≤ x) :
    ∑ p ∈ filter Prime (Iic ⌊x⌋₊), 1 / p = θ x / (x * log x) +
      ∫ y in 2..x, θ y * (1 + log y) / (y ^ 2 * log y ^ 2) := by
  sorry

[Pietro Monticone]

Fixed in PNT#651

[Pietro Monticone]

Oh, the same is true for pre_413. Let me add it to the same PR

[Pietro Monticone]

And eq_414, etc.

[Pietro Monticone]

Maybe we should add a red misformalisation label

[Pietro Monticone]

Done

[Pietro Monticone]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pulls?q=is%3Apr+is%3Aclosed+label%3Amisformalisation

[Pietro Monticone]

In SecondSummary.lean Aristotle proved:

theorem PT.corollary_2 : Eπ.classicalBound 235 1.52 0.8 1 (exp 2000)

theorem JY.corollary_1_3 : Eπ.classicalBound 9.59 1.515 0.8274 1 2

theorem Schoenfeld1976.has_prime_in_interval (x : ℝ) (hx : x > 2010760) :
    HasPrimeInInterval (x*(1-1/15697)) x

theorem RamareSaouter2003.has_prime_in_interval (x : ℝ) (hx : x > 10726905041) :
    HasPrimeInInterval (x*(1-1/28314000)) x

theorem RamareSaouter2003.has_prime_in_interval_2 (x : ℝ) (hx : x > exp 53) :
    HasPrimeInInterval (x*(1-1/204879661)) x

theorem GourdonDemichel2004.has_prime_in_interval (x : ℝ) (hx : x > exp 60) :
    HasPrimeInInterval (x*(1-1/14500755538)) x

theorem PrimeGaps2014.has_prime_in_interval (x : ℝ) (hx : x > exp 60) :
    HasPrimeInInterval (x*(1-1/1966196911)) x

theorem PrimeGaps2024.has_prime_in_interval (x : ℝ) (hx : x > exp 60) :
    HasPrimeInInterval (x*(1-1/76900000000)) x

and disproved:

theorem JY.theorem_1_4 : Eπ.vinogradovBound 0.028 0.801 0.1853 2

I'll open a PR soon.

[Pietro Monticone]

This is the disproof of JY.theorem_1_4:

theorem JY_thm_1_4_false : ¬ Eπ.vinogradovBound 0.028 0.801 0.1853 2 := by
  unfold Eπ.vinogradovBound;
  rw [ not_forall ];
  use 2; norm_num [ Eπ ];
  -- Substitute the values of $\pi(2)$ and $\mathrm{Li}(2)$ into the inequality.
  have h_pi2 : pi 2 = 1 := by
    unfold pi
    generalize_proofs at *;
    norm_num [ Nat.primeCounting ];
    decide +revert
  have h_Li2 : Li 2 = 0 := by
    unfold Li; norm_num;
  rw [h_pi2, h_Li2]
  norm_num;
  refine' lt_of_le_of_lt ( mul_le_mul_of_nonneg_right ( mul_le_of_le_one_right ( by positivity ) ( Real.rpow_le_one ( by positivity ) ( Real.log_two_lt_d9.le.trans ( by norm_num ) ) ( by norm_num ) ) ) ( Real.exp_nonneg _ ) ) _;
  exact lt_of_le_of_lt ( mul_le_mul_of_nonneg_left ( Real.exp_le_one_iff.mpr ( by norm_num ) ) ( by norm_num ) ) ( by have := Real.log_two_gt_d9; norm_num1 at *; linarith )

[Pietro Monticone]

@Terence Tao was it just a typo?

[Terence Tao]

I'll look into this. These results should not be provable yet, so there must be some exploit here, such as using some previous sorried result (perhaps the prime number theorem of Dusart)?

[Terence Tao]

OK, on checking against the original paper of Johnston and Yang, the threshold should be 23 instead of 2, it is indeed a typo. Thanks to you and Aristotle for pointing this out, I will fix it now.

[Pietro Monticone]

Opened PNT#739.

[Pietro Monticone]

Oh, let me fix the typo too.

[Pietro Monticone]

It's not using any decls from PrimeNumberTheoremAnd.Dusart, but it's using decls from PrimeNumberTheoremAnd.FKS2.

[Terence Tao]

OK, it seems the FKS2 prime number theorem is strong enough to imply a lot of older prime number theorems, which is a fact worth noting I guess, even though it is not the way these older theorems are "supposed" to be proved. It may be worth adding a remark in the blueprint comments that these results are currently being proven as a consequence of the stronger FKS2 result.

Eventually I would like to have independent proofs of these older theorems that follow the older arguments, in case one wants to do exploratory thought experiments such as "what is the best prime number theorem one could accomplish using only the numerical verification of RH available in 1996 (say)?", but these "cheap" proofs can serve as placeholders for now.

The proofs of the has_prime_in_interval statements are misformalizations though; I specified the endpoints of the interval containing primes when I should have specified the left endpoint and the length. As such, I accidentally made the intervals more or less of the form [x,2x] and so Bertrand's postulate (already in Mathlib) finished it off. Well, Aristotle again did its job of detecting misformalizations...

[Pietro Monticone]

Oh, I see. So, for example, Schoenfeld1976.has_prime_in_interval should be:

theorem Schoenfeld1976.has_prime_in_interval (x : ℝ) (hx : x > 2010760) :
    HasPrimeInInterval (x*(1-1/15697)) (x/15697) := by sorry

Right?

[Pietro Monticone]

Ok, fixed all the misformalised statements.

[Pietro Monticone]

The following was negated by Aristotle:

theorem Schoenfeld1976.has_prime_in_interval (x : ℝ) (hx : x > 2010760) :
    HasPrimeInInterval (x*(1-1/15697)) (x/15697)

[Pietro Monticone]

In particular:

/-
An entry (b, ε) is correct if Eπ(x) ≤ ε for all x ≥ exp(b).
-/
def FKS2.IsCorrectEntry (p : ℝ × ℝ) : Prop := ∀ x ≥ Real.exp p.1, Eπ x ≤ p.2

#eval (List.filter Nat.Prime (List.range' 2010700 300))

/-
Checking primes around 2010760.
-/
#eval (List.filter Nat.Prime (List.range' 2010700 300))

/-
The statement "For all x > 2010760, there is a prime in (x(1-1/15697), x]" is false.
-/
def HasPrimeInInterval_ (x h : ℝ) : Prop := ∃ p : ℕ, Nat.Prime p ∧ x < p ∧ p ≤ x + h

theorem Schoenfeld1976.counterexample : ∃ x : ℝ, x > 2010760 ∧ ¬ HasPrimeInInterval_ (x * (1 - 1/15697)) (x/15697) := by
  -- By definition of HasPrimeInInterval_, we need to show that there are no primes in the interval $(x(1-1/15697), x]$.
  unfold HasPrimeInInterval_;
  -- Set $x$ to be $2010880$.
  use 2010880;
  norm_num at *; -- Verify that $x > 2010760$.
  skip
  -- Check that there are no primes in the interval $(2010751.89..., 2010880]$.
  have h_no_primes : ∀ p : ℕ, Nat.Prime p → 2010752 ≤ p → p ≤ 2010880 → False := by
    intro p pp _ _; interval_cases p <;> norm_num1 at *;;
  use by
    exact fun p hp hp' => not_le.1 fun hp'' => h_no_primes p hp ( by rw [ div_lt_iff₀ ] at hp' <;> norm_cast at * ; linarith ) hp'';

/-
Checking if HasPrimeInInterval is defined.
-/
#check HasPrimeInInterval

/-
The statement "For all x > 2010760, there is a prime in (x(1-1/15697), x]" is false.
-/
theorem Schoenfeld1976.disproof : ∃ x : ℝ, x > 2010760 ∧ ¬ HasPrimeInInterval (x * (1 - 1/15697)) (x/15697) := by
  exact?

/-
The statement "For all x > 2010760, there is a prime in (x(1-1/15697), x]" is false.
-/
theorem Schoenfeld1976.disproof_v2 : ∃ x : ℝ, x > 2010760 ∧ ¬ HasPrimeInInterval (x * (1 - 1/15697)) (x/15697) := by
  -- By combining the results from theorem_3 and proposition_17, we can conclude that the statement is false.
  obtain ⟨x, hx⟩ := Schoenfeld1976.disproof
  use x

/-
The statement "For all x > 2010760, there is a prime in (x(1-1/15697), x]" is false.
-/
theorem Schoenfeld1976.disproof_v3 : ∃ x : ℝ, x > 2010760 ∧ ¬ HasPrimeInInterval (x * (1 - 1/15697)) (x/15697) := by
  exact?

/-
The statement "For all x > 2010760, there is a prime in (x(1-1/15697), x]" is false.
-/
theorem Schoenfeld1976.disproof_final : ∃ x : ℝ, x > 2010760 ∧ ¬ HasPrimeInInterval (x * (1 - 1/15697)) (x/15697) := by
  exact?

end AristotleLemmas

/-
def HasPrimeInInterval (x h : ℝ) : Prop := ∃ p : ℕ, Prime p ∧ x < p ∧ p ≤ x + h

**Schoenfeld 1976**

If $x > 2010760$, then there is a prime in the interval
  $$
  \left( x\left(1 - \frac{1}{15697}\right), x \right].
  $$
-/
theorem Schoenfeld1976.has_prime_in_interval (x : ℝ) (hx : x > 2010760) :
    HasPrimeInInterval (x*(1-1/15697)) (x/15697) := by
      -- Wait, there's a mistake. We can actually prove the opposite.
      negate_state;
      -- Proof starts here:
      -- Apply the theorem Schoenfeld1976.disproof_final to obtain the required x.
      obtain ⟨x, hx₁, hx₂⟩ := Schoenfeld1976.disproof_final;
      use x

[Terence Tao]

Ah, very interesting! On tracking down the source at Theorem 12 of this paper of Rosser https://www.jstor.org/stable/pdf/2005976.pdf , it looks like the actual statement is very slightly different: "the open interval $(x, x + x/16597)$ contains a prime for all $x \geq 2010759.9$". In terms of the notation of the repository, this would be

theorem Schoenfeld1976.has_prime_in_interval (x h : ℝ) (hx : x > 2010759.9) : HasPrimeInInterval x (x/15697) := by sorry

(Strictly speaking, this is an infinitesimally weaker statement because we permit the prime to be in the right endpoint of the interval, but I can't imagine this makes any actual difference in applications.) The description of this result in https://ramare-olivier.github.io/TME-EMT/Articles/Art09.html is therefore incorrect; I will submit a correction. In the meantime, would it be possible to run Aristotle against this revised version, and if it cannot find a counterexample, submit a PR to correct the statement?

On the positive side, this again demonstrates the value that formalization could add to the explicit analytic number theory literature!

[Pietro Monticone]

Terence Tao said:

In the meantime, would it be possible to run Aristotle against this revised version, and if it cannot find a counterexample, submit a PR to correct the statement?

Sure, I'll run it again soon.

[Pietro Monticone]

(deleted)

[Pietro Monticone]

(deleted)

[Pietro Monticone]

(deleted)

[Pietro Monticone]

(deleted)

[Pietro Monticone]

In Buthe.lean the following was negated by Aristotle:

theorem theorem_2f {x : ℝ} (hx1 : 2 ≤ x) (hx2 : x ≤ 10 ^ 19) :
    li x - pi x > 0

In particular:

theorem theorem_2f {x : ℝ} (hx1 : 2 ≤ x) (hx2 : x ≤ 10 ^ 19) :
    li x - pi x > 0 := by
      -- Wait, there's a mistake. We can actually prove the opposite.
      negate_state;
      -- Proof starts here:
      -- Let's choose $x = 2$.
      use 2; norm_num [li, pi];
      rw [ intervalIntegral.integral_undef ] <;> norm_num [ Nat.primeCounting ];
      rw [ intervalIntegrable_iff_integrableOn_Ioo_of_le ] <;> norm_num;
      -- We'll use the fact that $\int_{0}^{2} \frac{dt}{\ln t}$ diverges.
      have h_div : ¬ MeasureTheory.IntegrableOn (fun t : ℝ => (Real.log t)⁻¹) (Set.Ioo 1 2) MeasureTheory.MeasureSpace.volume := by
        -- We can compare our integral to the integral of $1/(t-1)$ over $(1, 2)$, which is known to diverge.
        have h_comparison : ∀ t ∈ Set.Ioo 1 2, (Real.log t)⁻¹ ≥ 1 / (t - 1) := by
          exact fun t ht => by rw [ ge_iff_le, inv_eq_one_div, div_le_div_iff₀ ] <;> nlinarith [ ht.1, ht.2, Real.log_pos ht.1, Real.log_le_sub_one_of_pos ( zero_lt_one.trans ht.1 ) ] ;
        -- Since $1/(t-1)$ is not integrable on $(1, 2)$, and $(Real.log t)⁻¹ \geq 1/(t-1)$ on this interval, it follows that $(Real.log t)⁻¹$ is also not integrable on $(1, 2)$.
        have h_not_integrable : ¬ MeasureTheory.IntegrableOn (fun t : ℝ => 1 / (t - 1)) (Set.Ioo 1 2) MeasureTheory.MeasureSpace.volume := by
          rw [ ← intervalIntegrable_iff_integrableOn_Ioo_of_le ] <;> norm_num;
        refine fun h => h_not_integrable <| h.mono' ?_ ?_;
        · exact Measurable.aestronglyMeasurable ( by exact Measurable.div measurable_const ( measurable_id.sub measurable_const ) );
        · filter_upwards [ MeasureTheory.ae_restrict_mem measurableSet_Ioo ] with t ht using by rw [ Real.norm_of_nonneg ( one_div_nonneg.mpr ( sub_nonneg.mpr ht.1.le ) ) ] ; exact h_comparison t ht;
      exact fun h => h_div <| h.mono_set <| Set.Ioo_subset_Ioo ( by norm_num ) le_rfl

[Pietro Monticone]

In SecondSummary.lean Aristotle proved CarneiroEtAl2019RH.has_prime_in_interval:

theorem interval_subset_prime {x A B : ℝ} (hA : HasPrimeInInterval (x - A) A) (hAB : A ≤ B) :
    HasPrimeInInterval (x - B) B := by proof

theorem CarneiroEtAl2019RH.has_prime_in_interval (x : ℝ) (hx : x ≥ 4) (RH : RiemannHypothesis) :
    HasPrimeInInterval (x - (22 / 25) * sqrt x * log x) ((22 / 25) * sqrt x * log x) := by
      -- For $x \geq 6.2$, we use Theorem \ref{rh_prime_interval_2002}.
      by_cases hx_ge_6_2 : x ≥ 6.2;
      · -- By `RHPrimeInterval2002.has_prime_in_interval`, there is a prime in $(x - 1.6\sqrt{x}, x]$.
        have h_prime_interval_2002 : HasPrimeInInterval (x - (8 / 5) * Real.sqrt x) ((8 / 5) * Real.sqrt x) := by
          convert RHPrimeInterval2002.has_prime_in_interval x ( by linarith ) RH using 1
        -- Since $0.88 \sqrt{x} \log x \geq 1.6 \sqrt{x}$ for $x \geq 6.2$, we can apply `interval_subset_prime`.
        have h_subset : (22 / 25) * Real.sqrt x * Real.log x ≥ (8 / 5) * Real.sqrt x := by
          -- We can divide both sides by $Real.sqrt x$ (which is positive since $x \geq 4$).
          have h_div : (22 / 25) * Real.log x ≥ (8 / 5) := by
            -- We'll use that $Real.log x \geq Real.log 6.2$ for $x \geq 6.2$.
            have h_log_ge : Real.log x ≥ Real.log 6.2 := by
              exact Real.log_le_log ( by norm_num ) hx_ge_6_2
            -- We'll use that $Real.log 6.2 \approx 1.82$.
            have h_log_6_2 : Real.log 6.2 > 1.82 := by
              norm_num [ Real.log_lt_log ] at *; (
              rw [ div_lt_iff₀' ] <;> norm_num [ ← Real.log_rpow, Real.lt_log_iff_exp_lt ];
              have := Real.exp_one_lt_d9.le ; norm_num1 at * ; rw [ show Real.exp 91 = ( Real.exp 1 ) ^ 91 by rw [ ← Real.exp_nat_mul ] ; norm_num ] ; exact lt_of_le_of_lt ( pow_le_pow_left₀ ( by positivity ) this _ ) ( by norm_num ) ;)
            norm_num at * ; linarith [ Real.log_le_sub_one_of_pos ( show 0 < 6.2 by norm_num ) ] ;
          nlinarith [ Real.sqrt_nonneg x ]
        exact interval_subset_prime h_prime_interval_2002 h_subset |> fun h => by simpa only [ neg_sub ] using h;
      · -- For $4 \leq x < 6.2$, we consider $p=3$ and $p=5$.
        by_cases hx_ge_5 : x ≥ 5;
        · -- For $5 \leq x < 6.2$, we consider $p=5$.
          use 5
          norm_num at *;
          exact ⟨ by nlinarith [ show Real.log x ≥ 1 by exact Real.le_log_iff_exp_le ( by linarith ) |>.2 <| by exact Real.exp_one_lt_d9.le.trans <| by norm_num; linarith, show Real.log x ≥ 1 by exact Real.le_log_iff_exp_le ( by linarith ) |>.2 <| by exact Real.exp_one_lt_d9.le.trans <| by norm_num; linarith, Real.sqrt_nonneg x, Real.sq_sqrt <| show 0 ≤ x by linarith ], hx_ge_5 ⟩;
        · -- For $4 \leq x < 5$, we consider $p=3$.
          have h_prime_3 : HasPrimeInInterval (x - (22 / 25) * Real.sqrt x * Real.log x) ((22 / 25) * Real.sqrt x * Real.log x) := by
            have h_prime_3_interval : x - (22 / 25) * Real.sqrt x * Real.log x < 3 := by
              -- We'll use that $Real.log x \geq Real.log 4$ for $x \geq 4$.
              have h_log_ge_log4 : Real.log x ≥ Real.log 4 := by
                exact Real.log_le_log ( by norm_num ) hx
              rw [ show ( 4 : ℝ ) = 2 ^ 2 by norm_num, Real.log_pow ] at h_log_ge_log4 ; norm_num at * ; nlinarith [ Real.sqrt_nonneg x, Real.sq_sqrt ( show 0 ≤ x by linarith ), Real.log_two_gt_d9, Real.log_le_sub_one_of_pos zero_lt_two ]
            exact ⟨ 3, by norm_num, h_prime_3_interval, by linarith ⟩
          grind

[Pietro Monticone]

Opened PNT#746

[Pietro Monticone]

Opened PNT#747

[Terence Tao]

Ah, Aristotle has uncovered some further misformalizations. RHPrimeInterval2002.has_prime_in_interval and Dudek2015RH.has_prime_in_interval are missing log x factors after the sqrt x factors (see Section 2 of https://ramare-olivier.github.io/TME-EMT/Articles/Art09.html ). Sorry about this (was not reviewing the AI-generated output carefully enough).

Aristotle's negation of Buthe's theorem uncovered another misformalization: I had defined the logarithmic integral li as

noncomputable def li (x : ℝ) : ℝ := ∫ t in 0..x, 1 / log t

but 1/ log t actually has a singularity at t=1 and this limit needs to be evaluated in a principal value sense. Many papers use the variant

noncomputable def Li (x : ℝ) : ℝ := ∫ t in 2..x, 1 / log t

to avoid this.

I will submit a PR now to fix this. It does mean that one of the already formalized lemmas, namely li x = Li x + li 2 for x>2, will need a new proof unfortunately.

[Pietro Monticone]

@Terence Tao Of course feel free to push the fixes directly in the related opened PRs by adding the misformalisation label

[Terence Tao]

OK I updated PNT#749 with fixes

[Pietro Monticone]

Updated title and PR description

[Pietro Monticone]

Artistotle helped me to find another misformalised statement (task PNT#767):

theorem symm_inv_log
    (t : ℝ) (ht : 0 < t) (ht' : t ≤ 1 / 2) :
    |1 / log (1 + t) + 1 / log (1 - t)| ≤ log (4 / 3) / (4 / 3)

with a counterexample at t = 1/2.

I’ll open a PR soon to fix it.