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.
