Goldbach's conjecture(s) - a challange for (open)AI?

[Alexander van der Vekens]

Although the binary Goldbach conjecture (claiming that every even number (greater than 4) is the sum of two (odd) primes) is not proven yet, the ternary Goldbach conjecture (claiming that every odd number (greater than 7) is the sum of three (odd) primes) seems to be proven by Harald Helfgott in 2014.  It would be great if this proof can be formalized with Metamath (although it is not in the Metamath 100 list), providing the still missing official acceptance (usually obtained by a publication in a peer-reviewed journal). 

I provided some definitions (of even resp. odd Goldbach numbers) and some related theorems in my latest contributions to set.mm, see section "Goldbach's conjectures" in my mathbox. This section should be a starting

point for the formal proofs of the Goldbach conjectures. The main problem will be to provide means to express the results from checking "small" numbers (performed with a computer): numbers up to about 4 x 10^18 for the binary Goldbach conjecture resp. about 9 x 10^30 for the ternary Goldbach conjecture.  Maybe each of the results must be provided as theorem, like ~ 6gbe , which would be quite a lot...

Finally I formulated the binary Goldbach conjecture and the ternary Goldbach conjecture at the end of the section - of course they are in comments, because they are not (formally) proven (yet): ~goldbach resp. ~tgoldbach.

Although I do not believe that neither the ternary nor the binary Goldbach conjecture will be proven using Metamath in the next years (decades?), I still have the hope and the vision that this will happen some day, maybe with the help of AI. For the time being, I wonder if these theorems could be already a challange for openAI, showing its power or its limits.

Everybody is invited, of course, to contribute more theorems/lemmas which will help to reach this goal.

Best regards,

Alexander

[Stanislas Polu]

Hi Alexander,

Challenge accepted! :)

(I'm off until the end of next week but wanted to acknowledge your
message early. So please excuse my short response/reaction, I'll work
on a much proper one as I come back)

I'm unfamiliar with Helfgott's proof in particular the need for
bootstrapping with "small" numbers. Do you have a preferred reference
to share for us to get more familiar with the ternary conjecture
(which would be such an exciting achievement if our systems were to
help here).

(Truth be told, I've been closely following your recent PRs with the
exact motivation you state in your email so I was quite excited to
find out your message tonight)

Best,

-stan

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7767d7db-e3ce-4e15-ab66-e4c42766654eo%40googlegroups.com.

[Alexander van der Vekens]

Hi Stan,

you can find a reference to Helfgott's paper on the MPE Homepage http://us.metamath.org/mpeuni/mmset.html (see [Helfgott]). I think all required definitions are contained (or at least referenced) in this paper. This paper has about 80 pages, the proof itself takes about 60 pages, but I think it is not complete in every detail (there are a lot of references to related papers...). Therefore I think it is really a big challange to prove it with Metamath.

Alexander

[savask]

The main problem will be to provide means to express the results from checking "small" numbers (performed with a computer): numbers up to about 4 x 10^18 for the binary Goldbach conjecture resp. about 9 x 10^30 for the ternary Goldbach conjecture.  Maybe each of the results must be provided as theorem, like ~ 6gbe , which would be quite a lot...

The proof of ~6gbe takes about 500 bytes in set.mm, so recording Goldbach partitions of all even numbers up to 4x10^18 will require at least 10^21 bytes, i.e. a zettabyte. For comparison, that is more or less on the same order of magnitude as the amount of data generated worldwide (see https://en.wikipedia.org/wiki/Zettabyte#Comparisons_for_scale). At this point AI would have a better chance trying to lower this bound to something more feasible :-)

[Mario Carneiro]

Helfgott's main paper says that the paper proof covers C >= 10^27, so numerical verification of ternary Goldbach is required up to 10^27. However, according to the first page of https://arxiv.org/pdf/1305.3062.pdf (the reference for the computation of the low part), to get this bound it suffices to prove the Riemann Hypothesis up to at least 3 x 10^10. The reference https://people.maths.bris.ac.uk/~madjp/thesis5.pdf cited doesn't explicitly mention this number (it mentions a smaller number for GRH that might be convertible to RH), but the results that are there seem to suggest that there were about 10^9 low to high precision integrals (most low, a few high) needed to establish the main result. This puts it within the range of modern computers, which is why we have the result in the first place.

Of course, if it's *just* within the range of modern computers to prove this, then it is out of range for formal verification, at least encoded naively as a metamath proof, because there is no way to do that without some overhead. However, in the original context it is not known, for example, which integrals are low precision and which are high, and an oracle for that can possibly decrease the verification time by lowering the low precision baseline even further and pointing out how high is necessary for the high precision integrals.

However, I think that most of Helfgott's proof is well out of reach of metamath at the moment, not because of the computations but because there is a *significant* mathematics gap of analytic number theory required to do the proof for C large, as well as the reduction from TGB to RH and from RH to some concrete calculations. It seems the key step is the https://en.wikipedia.org/wiki/Hardy%E2%80%93Littlewood_circle_method , which might be in range given the similarities to the method used to calculate the integrals in the prime number theorem. This then goes through a bunch of precise estimates, which probably differ significantly in their difficulty. The hard part here is I think just getting through all of them - Helfgott has hundreds of pages of integrals. But I think that this part is easier than the RH verification part in terms of computational power.

But this is the sort of proof that I would really like to have a reflective verifier for. It makes a lot of sense and is a lot better use of hardware to prove correctness of a program and then run it, and all that is needed to make this just as good a proof as the raw exprs proof is a proof that the reflective verifier is conservative over a standard verifier, which can be performed in a verified metalogic (aka MM0's strategy). (I'm not sure exactly how to calculate where the best cutoff point is for where standard proof loses to reflective proof, because it involves a time-space tradeoff: the standard proof will probably take less time to check, but the reflective verifier does not need massive proofs on disk. Actually, considering that memory and disk are much slower than computation at the moment, in addition to the fact that computation in metamath involves relatively low bases and lots of memory accesses, I am pretty sure that standard proof is at least a hundred times slower than reflective proof when it comes to pure number crunching, so there isn't really any tradeoff at that level. When the verified program becomes more "searchy", the standard proof starts to win because it has an oracle giving all the right answers, but a reflective proof can have the best of both worlds here, by verifying a certificate.)

Mario

On Fri, Aug 7, 2020 at 5:45 AM savask <sav...@yandex.ru> wrote:

The main problem will be to provide means to express the results from checking "small" numbers (performed with a computer): numbers up to about 4 x 10^18 for the binary Goldbach conjecture resp. about 9 x 10^30 for the ternary Goldbach conjecture.  Maybe each of the results must be provided as theorem, like ~ 6gbe , which would be quite a lot...

The proof of ~6gbe takes about 500 bytes in set.mm, so recording Goldbach partitions of all even numbers up to 4x10^18 will require at least 10^21 bytes, i.e. a zettabyte. For comparison, that is more or less on the same order of magnitude as the amount of data generated worldwide (see https://en.wikipedia.org/wiki/Zettabyte#Comparisons_for_scale). At this point AI would have a better chance trying to lower this bound to something more feasible :-)

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2e121181-6739-4bbb-9c20-6404f1280caeo%40googlegroups.com.

[Abhishek Chugh]

This problem obviously highlights the opportunities for metamath that would open up by embracing computational-based paradigms. I think metamath should add the concept of verification certificate (something like Mario's suggestion) - that can be added into the metamath databases as a reference.

FWIW, my suggestion would be to sidestep the computation problem for now by simply adding an axiom which states GBC is true for all numbers < 10^31. This axiom could live in a mathbox or if we want to be really careful, in a copy of set.mm

IMO, such a 'conditional' formal proof would end-up helping the proof getting published in a peer-reviewed journal (or maybe we will find a flaw in the proof). In any case, it would be a huge win for Metamath and OpenAI. The good press metamath will get with the proof will help more people get to solve the limitations of metamath.

[Mario Carneiro]

You don't need to call it a "conditional formal proof", it's a proof of the asymptotic ternary goldbach theorem, which is a famous result by Vinogradov (https://en.wikipedia.org/wiki/Vinogradov%27s_theorem). It is true that Helfgott improved this but it's essentially the same method, only with more refined estimates in order to bring the lower bound within reach of computers.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/63183c9c-7120-4c8e-a75d-8a61af54c358o%40googlegroups.com.

[Thierry Arnoux]

On the path to the Hardy-Littlewood circle method, at the center of Goldbach’s conjecture, Is Cauchy’s residue theorem, which is on the list of obvious omissions to the 100 theorems to be formalized. We should probably start with a formalization of the line (contour) integrals. One of the building blocks could be Jeff Madsen’s definition of path concatenation (df-pco), and Mario’s developments.

So the path would be:
- Line integrals
- Cauchy’s Residue Theorem
- Hardy-Littlewood circle method
- Goldbach’s conjecture

If we want to try an “OpenAI” collaborative method, maybe experienced Metamath users could post definition and theorem statements, letting OpenAI fill-in the proof?

From my experience playing with the OpenAI proof assistant, it is quite good at filling in the blanks automatically, but did not suggest with a high confidence the main proof steps. That should complement very well a human, who sees well the big picture and the main steps, but is much more inefficient in those smaller steps. Maybe the proof statements could be completed with the main proof steps?
BR,
_
Thierry

[savask]

On the path to the Hardy-Littlewood circle method, at the center of Goldbach’s conjecture, Is Cauchy’s residue theorem, which is on the list of obvious omissions to the 100 theorems to be formalized. We should probably start with a formalization of the line (contour) integrals.

Although it is true that the original Hardy-Littlewood method requires complex analysis, nowadays it's often formulated in the language of exponential sums. In particular, Vinogradov's proof of Goldbach ternary conjecture for large numbers does not require Cauchy's theorem or any complex analysis whatsoever (so good-old ~df-itg is enough).

That being said, it does require Siegel-Walfisz theorem (an asymptotic for the sum of log p for primes p = a (mod n)). I'm not sure if there's an elementary proof of that result and if it (possibly) could be derived from metamath's current treatment of Dirichlet's theorem.

One can of course start with a simpler application of the circle method, for instance, with Waring's problem. It's solution is more or less elementary and sure many intermediate results will prove to be useful in the formalization of Vinogradov's (or Helfgott's) proof.

[Jon P]

Just a note on this point

> If we want to try an “OpenAI” collaborative method, maybe experienced Metamath users could post definition and theorem statements, letting OpenAI fill-in the proof?

I would benefit from this a lot I think. I struggle to know where the frontiers of MM are, how to formally state a theorem and how to find the informal proofs to build from. If people posted theorem statements and I could have a go at them I'd really like that. I also like playing with the OpenAI tool, and am still not so good with it, solving Filip's problem 4 took 10 attempts.

I also think it might help with a pipeline for new people, 1. do the practice problems, 2. try some of the theorems which are stated and unproven, 3. find a field you would like to expand yourself. That way people can learn the skills a few at a time. This sort of discussion in this thread, about how to approach some new territory, is a very high level skill which requires already understand how to prove things well I think.

[Thierry Arnoux]

That being said, it does require Siegel-Walfisz theorem (an asymptotic for the sum of log p for primes p = a (mod n)).

Thank you Savely!

I think a lot of Mario's material from the Prime Number Theorem can be used as a basis, including von Mangoldt's and Euler's phi functions. Mario also mentioned the methods to compute the integrals might be similar.

What about Nathanson, Melvyn B. (1996). Additive number theory. The classical bases (ISBN 0-387-94656-X): could we use this textbook as a reference?

BR,
_
Thierry

[savask]

What about Nathanson, Melvyn B. (1996). Additive number theory. The classical bases (ISBN 0-387-94656-X): could we use this textbook as a reference?

I think it's an excellent reference, very detailed and self contained for the most part. It has some occasional typos/errors (what doesn't?) and does not prove facts like Siegel-Walfisz theorem; Waring's problem does not require that result, so it shouldn't be a problem at the beginning.