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 On Thursday, August 6, 2020 at 10:25:39 PM UTC+2 [email protected] wrote: > 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 > > On Thu, Aug 6, 2020 at 9:29 PM 'Alexander van der Vekens' via Metamath > <[email protected]> wrote: > > > > 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 > > > > -- > > 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 [email protected]. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/7767d7db-e3ce-4e15-ab66-e4c42766654eo%40googlegroups.com > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/919fcc8e-5e16-4570-b7b8-e34a19fb4ac1n%40googlegroups.com.
