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.
On Fri, Aug 7, 2020 at 7:50 PM Abhishek Chugh <[email protected]> wrote: > 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. > > -- > 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/63183c9c-7120-4c8e-a75d-8a61af54c358o%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/CAFXXJSuKzxFUQCWc0mUembCvxp6RR_1KtUf886bP9_1vYwygbw%40mail.gmail.com.
