New miniproject: Primes in short intervals

Stream: PrimeNumberTheorem+

[Terence Tao]

I have created tasks (PNT#900 - PNT#913), spread out across a number of Lean files, to formalize a "pipeline" from prime number theorems (and specifically, upper bounds on the quantity $E_\theta(x) := |\theta(x)-x|/x$) and "prime number theorems in short intervals", which guarantee the existence of at least one prime $p$ in the range $x < p \leq x+h$ for various $x, h$. The deduction of the latter from the former is not terribly difficult, but in practice it does involve a certain amount of case analysis and computation which is very suitable for formalizing in Lean. I also note that the FKS2 paper that we are formalizing produces upper bounds on $E_\theta$ as one of its outputs, and the LCM project that is completely formalized requires a prime number theorem in short intervals as its sole input, so this new pipeline connects the two together.

Several files have either been created or updated to manage this project:

• Defs.lean This file contains many basic definitions that previously were scattered across the repository, sometimes redunantly. In particular it now carries the notion of an "admissible bound" $A (\log x/R)^B \exp( - C \sqrt{\log x/R} )$, which is a typical bound one gets in prime number theorems with error terms. PNT#900 PNT#901 establishes some basic monotonicity properties of these bounds, and in particular can convert "classical" prime number theorems to "numerical" prime number theorems that state things like $E_\theta(x) \leq \varepsilon$ for $x \geq x_0$ for various $x_0, \varepsilon$.
• eSHP_tables.lean eSHP.lean These contain some numerical results of e Silva, Herzog, and Pardi regarding prime gap records, recording things like the first appearance of a prime gap larger than all preceding prime gaps. The numerics scan primes as large as $10^{18}$ and the full verification of the tables would be completely infeasible in Lean. However, as a "unit test", I have opened PNT#902 PNT#903 to verify these tables for the primes up to 30. Here I am adopting a similar structure in some other Lean files of moving all the numerical tables to a separate file with significantly fewer imports, so that purely numerical calculations involving those tables can be performed with only very infrequent needs to recompile (once per mathlib update, basically).
• PrimeInInterval.lean This file contains a number of elementary theoretical results that convert either bounds on $E_\theta$ or results on prime gap records into theorems on primes in short intervals. PNT#904 PNT#905 PNT#906 PNT#907 PNT#908 PNT#909 contain a number of small tasks to formalize these easy conversions.
• Dusart.lean had previously existed, and contained in particular a theorem about primes in short intervals (Proposition 5.4) that was the main input for LCM.lean. PNT#910 PNT#911 PNT#912 PNT#913 establishes this theorem (and a corollary of it) as a consequence of a prime number theorem with classical error term, together with prime gap records, together with an additional numerical verification for small $x$ (in the range $89693 \leq x \leq 360353$), which is another numerical computation that is infeasible to formalize fully in Lean.

Most of these tasks are quite small and would be suitable for beginners or for AI tools.

NOTE: due to the addition of all the new files, blueprint numbering has changed somewhat. I have updated the numbering in all unclaimed issues to match this, but claimed issues may now have some discrepancy with the numbering of theorems, lemmas, and definitions. The URL links should still work as expected, though.

[Aayush Rajasekaran]

Here is a PR for PNT#912. Please note the minor changes to proposition_5_4b and proposition_5_4c.

[Aayush Rajasekaran]

@Alejandro Radisic I attempted a golf of your proof of proposition_5_4a -- here is the PR. I think it sacrifices some readability, but curious what you think.

[Alejandro Radisic]

@Aayush Rajasekaran I think the tradeoff is readability/auditability in proposition_5_4a, since a few conceptual steps are more compressed now. IMO a good middle ground is to keep this shorter structure but keep a few named intermediate facts (hE2 via log monotonicity, hlog_big, hcoeff) so it stays easier to maintain and debug. Either version is fine with me

[Terence Tao]

It turns out that the formalization of the prime gap record tables from [eSHP] was incomplete: while we had formalized that every entry in the tables was a prime gap record, we did not formalize the converse statement that every prime gap record below a certain size was in the tables. It is this converse direction that is actually needed for applications. While this converse direction is too large a computation to be feasible to formalize in Lean, I have created some small unit test tasks PNT#948 PNT#949 PNT#950 PNT#951 to ensure that the definitions are formalized correctly, and lead to the expected conclusions (e.g., an upper bound of 1476 for all the prime gaps up to $4 \times 10^{18}$).

[J. J. Issai (project started by GRP)]

I look forward to seeing the project confirm that all gaps below $68\times 10^{18}$ are at most 1676 (c.f. https://en.wikipedia.org/wiki/Prime_gap). (Hope it won't be too long a wait.)

[Terence Tao]

Perhaps I should clarify that these proofs will not be unconditional,and will assume that the tables in [eSHP] are accurate. As a unit test I asked to verify these prime gap tables for the primes up to 30, but I definitely do not expect these proofs to scale up to anything close to 10^18 or more.

[Kevin Buzzard]

As I've said before, I think that these would be very good independent projects for people who know more about the computer programming side of Lean to attack. If there could be some concrete goals about prime numbers whose proof is a large computation and which have applications in this project then perhaps there would be some interest from others. Things like "write a good primality proving algorithm" and "see if we can check some basic statement about prime gaps up to 10^9" seem like interesting questions.

[Bhavik Mehta]

https://github.com/b-mehta/PrimeCert by me and Kenny does the primality proving bit, I'm working on making it easier to import and also bringing it to mathlib. (It already doesn't use any native_decide). Earlier versions of this code were used for the LCM stuff, for 40 digit primes, but it can comfortably handle 60 digit primes too. A much, much earlier version of this code (perhaps 4 years ago, in Lean 3) verified Goldbach up to 10^5; I haven't tested it yet but I expect it could go a lot higher these days.
It's currently optimised for verifying primality of specific large primes, however, rather than producing proofs of the form "all primes q between [1, x] satisfy P(q)". For the latter, perhaps a sieve-based idea might be better, but more experimentation is needed.