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/8c88ceb6-26a0-4130-896d-545888c1b3d6n%40googlegroups.com. -- 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/BE5BF842-9164-4C51-8421-AC52084A3DE0%40panix.com.
