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/CACZd_0z%2BrE44ZL%2BN7i4D%3DKokFxD%3DgVPVQdx52-xXKCBkfNgR5A%40mail.gmail.com.
