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.
[email protected] schrieb am Samstag, 23. November 2024 um 20:06:30 UTC+1: > 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. > > > On November 23, 2024 9:58:32 AM PST, Steven Nguyen <[email protected]> > wrote: > >> 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/ee7c8940-3e59-48c5-bc8d-67ad2e2d984bn%40googlegroups.com.
