Just a note on this point > If we want to try an “OpenAI” collaborative method, maybe experienced Metamath users could post definition and theorem statements, letting OpenAI fill-in the proof?
I would benefit from this a lot I think. I struggle to know where the frontiers of MM are, how to formally state a theorem and how to find the informal proofs to build from. If people posted theorem statements and I could have a go at them I'd really like that. I also like playing with the OpenAI tool, and am still not so good with it, solving Filip's problem 4 took 10 attempts. I also think it might help with a pipeline for new people, 1. do the practice problems, 2. try some of the theorems which are stated and unproven, 3. find a field you would like to expand yourself. That way people can learn the skills a few at a time. This sort of discussion in this thread, about how to approach some new territory, is a very high level skill which requires already understand how to prove things well I think. -- 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/b6cadc1c-8eb0-4481-921a-757f9782ee38o%40googlegroups.com.
