I think one of the benefits of "Formalizing 100 Theorems" is that it spurns development, but the remaining theorems in Metamath 100 are rather far away. So I had ChatGPT generate a bunch of other theorems:
https://chatgpt.com/share/674215c7-8c58-800c-b2b8-e7bb5c1ddfce Obviously this is incredibly arbitrary and the phrase "Metamath 200" should not be used, but that's the general idea. This strategy will probably be useful for future me whenever I'm stuck or my mind is blank, which I think is caused by most textbooks not being in the sweet spot of being exactly the next step for the library to progress. -- 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 visit https://groups.google.com/d/msgid/metamath/8c88ceb6-26a0-4130-896d-545888c1b3d6n%40googlegroups.com.
