New subproject: Odd goldbach for small n

Stream: PrimeNumberTheorem+

[Terence Tao]

Started a quick application of the primes in short intervals machinery already in PNT+: by a standard argument, once one knows some theorems about primes in short intervals, one can bootstrap numerical verification of the even Goldbach conjecture (all even numbers greater than 2 are the sum of two primes) to numerical verification of the odd Goldbach conjecture (all odd numbers greater than 5 are the sum of three primes). For instance, Ramare and Saouter used a verification of Richter of the even Goldbach conjecture up to $4 \times 10^{14}$, together with a short interval theorem, to conclude verification of the odd Goldbach conjecture up to $1.13256 \times 10^{22}$. I have some initial tasks for this at PNT#959 PNT#960 PNT#961 PNT#962 and will add a few more later. (EDIT: this is now done: PNT#769 PNT#770)

[Harald Helfgott]

The alternative would be to construct a prime-number ladder (as we did in Helfgott-Platt; this is an old strategy). It was a weekend computation on a Mac Mini sitting on my bedroom desk, even back in 2013, so I don't necessarily think that would be unrealistic to formalize.

[Terence Tao]

Hmm, suppose for instance we used the even Goldbach verification up to $4 \times 10^{18}$ and wanted to use a ladder to verify up to, say, $4 \times 10^{30}$. Then one would need a ladder of about $10^{12}$ primes of size $\sim 10^{30}$, and to verify the ladder one needs to check that they are all prime (and that they are spaced by less than $4 \times 10^{18}$. The spacing seems doable within Lean, but I'm not sure that Lean's primality testing algorithms are sufficient for this task (even if using native_decide). These are the sort of inputs though that I am happy to trust rigorous code (e.g., using interval arithmetic to handle any real numbers that show up) to handle rather than Lean.

[Johan Commelin]

What are the primality certificates typically used at such a scale?

[Kevin Buzzard]

I've seen @Bhavik Mehta proving numbers are prime in Lean in that range using Pratt certificates IIRC (in a talk at Imperial). Bhavik have I remembered correctly?

[Bhavik Mehta]

Yeah, for numbers up to 50 digits Pratt certificates work great. Kenny extended my work to use Pocklington certificates (in https://github.com/b-mehta/PrimeCert) so it now comfortably handles 70 digit primes.
The (slower) Pratt certificate code is what I used for the LCM highly abundant ladder (here: #PrimeNumberTheorem+ > Explicit estimates: $$M(x)$$, $$\psi(x)$$ @ 💬) which is a chain of primes up to $10^{40}$, and it's reasonably efficient. And (as people who know me well will know) none of this uses native_decide.

[Bhavik Mehta]

I don't have an estimate off the top of my head on how fast a ladder of $10^{12}$ primes of 30 digits would take to verify. But a computation which took under 48 hours on 2013 seems like it should be reasonable to verify in under 48 hours today. I'm on vacation this week, but I can take a look next week.

[Harald Helfgott]

What Platt and I did was use Proth primes, which are easy to certify.

[Bhavik Mehta]

Ah right, the code should already be pretty efficient for those: I think I did a 400 or so digit example a while ago

[Terence Tao]

But one would still need to include a list of 10^{12} primes somewhere in the Lean files, unless one uses the IO functions, right? This feels a bit too risky to have in the main project, both for build time and for security reasons, but perhaps it would be fine to have in a completely separate Lean repository. (Harald, I don't know if you have saved the file of primes from your 2013 work with Platt, but presumably with modern computers (and AI) one should be able to regenerate a comparable list relatively quickly.)

[Harald Helfgott]

Hm, I may have access to the backup drive of that ancient Mac Mini in early March, but I can ask Platt. (Each of us wrote a program and ran it separately.) I don't think I kept a list of the primes - that would have been too much memory.

[Harald Helfgott]

I'm sure I still have the code somewhere.

[Harald Helfgott]

Found my code. Right, I'm definitely not storing the list.

[Johan Commelin]

Yeah, that would be ~40 TB, right? Sounds a bit too large for a random Lean file :see_no_evil:

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

So store differences between consecutive list members. That should get it down easily to under ~30 TB.

[Harald Helfgott]

Excuse my ignorance, but why would a proof by brute force via Lean have to store all the primes in the file? Is it because that would necessarily be part of some sort of certificate? I would have thought the code would need to typecheck once and do the computation as part of that process, but not store all of the primes.

This feels like a newbie question, but also one that will help me understand something about Lean I haven't yet understood.

[Johan Commelin]

It's not necessary, and indeed probably not a good idea.
It's a tradeoff between time and memory. Computing the primes on the fly will be more work but will save a lot on space.

[Harald Helfgott]

Then don't do it. It's not like computing zeros of zeta(s), where the zeros themselves will be useful for a ton of other things. This isn't a large computation by any stretch of the imagination - and at any rate, having a ladder up to 10^27 (probably a lot less than that, once I am done improving certain things...) will be enough. If that feels like too small a task, then compute a ladder up to 10^27 with smaller gaps. It's the verification of binary Goldbach up to 4*10^18 that is genuinely a large computation.

[Terence Tao]

Ah, right, the statement one would be typechecking does not have to retain the proof (thanks to propositional extensionality) and so one does not need to keep the primes around as a certificate.

It may be premature to actually implement any of this in some lean repository now, but it could be an interesting intellectual exercise to estimate what type of time/memory requirements would be needed to hypothetically verify in Lean that for every $N \leq 10^{30}$ (say), there exists a prime between $N$ and $N + 4 \times 10^{18}$.

[Harald Helfgott]

Not to repeat myself, but, as I just implied, it would make perhaps more sense to estimate up to which point it would be realistic to verify binary Goldbach in Lean ($L=10^{15}$, say?) and then see what type of requirements would be needed to verify that for every $N\leq 10^{25}$ or $N\leq 10^{27}$ there exists a prime between $N$ and $N+L$.

[Terence Tao]

I would imagine the former task scales essentially linearly in $L$ and the latter task scales essentially inversely in $L$, so the geometric mean between the run time for these two tasks (for a reasonable choice of $L$) would be a good proxy for the total optimized run time.

On the other hand I would imagine that the modern explicit prime number theorems at medium ranges would already handle the latter task without any further numerics, in the spirit of the Kadiri-Lumley paper.

[Harald Helfgott]

Agreed on the scaling. On the second matter: the best explicit prime number theorems will give you the existence of primes between $N$ and $N+L$ when $L\gtrsim \pi N/H$ or so, where $H$ is the height up to which you have verified RH. (You get $2\pi N/H$ from Chirre-Helfgott off-the-shelf, but perhaps one can lop off that $2$.) The uncertainty principle pays us a visit again.

Of course then the question is up to where is it realistic to verify RH by formal means nowadays, bearing in mind that that's something in which it is worthwhile to sink resources, compared to a special-purpose computation.