Metamath 200

[Steven Nguyen]

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.

[Jim Kingdon]

I suppose the Equational Theories Project would be too much work to be a Metamath project? <https://mathstodon.xyz/@tao/113522452070896956>

I mean, they did have 50+ contributors who spent several months formalizing this in Lean. I guess on the positive side a Metamath project would have the Lean proofs to refer to. Plus it would appear to be readily amenable to breaking down into subtasks.

[Alexander van der Vekens]

I  made a similar attempt 5 years ago to provide more theorems which could be proven by Metamath, see https://groups.google.com/g/metamath/c/9U6m_MRmtx0/m/cfezBXDEAQAJ.

Of course, such lists can be helpful to add more "knowledge" (proof) to our knowlage base set.mm.