"Do you believe the community would be interested in an online tool to discharge goals?"
Personally I think an AI assisted proof tool would be really cool. I also think it could be really helpful for getting new people into MM. If there were a dozen easy problems people could do to start going, like Filip's ones which are nice, that would help beginners I think. Then when trying harder things the AI could make suggestions or offer to finish the proof when they are close. -- 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/15e52cef-a2d5-45b8-abf6-0ddc2f8d08ad%40googlegroups.com.
