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.
