> I think it would be beneficial for the Metamath community to have such a tool, too. I've been thinking about it for a while.
Thierry, I've been also thinking that Metamath could benefit from some collaboration, but I came to the conclusion that currently Metamath community is probably too small. It seems that there are lot more people involved in Lean, there are Lean-oriented courses at universities and there are people who do Lean nearly full-time (the closest we had to such a person was Mario, but it seems he has moved to other projects). Needless to say, Lean has better tooling and PA tactics. I can't speak for others, but I personally don't attempt formalizing theorems myself anymore precisely because one has to spend a ridiculous amount of effort to formalize trivial things, like doing algebraic manipulations or proving tautologies. That sounds too grim, but I like your "This gives a good overview of the steps to reach the goal, and everyone can grab a piece" idea :-) Maybe we could try to foster some collaboration by following Norm's suggestion <https://groups.google.com/g/metamath/c/5vbEj2vnvAg/m/eJ5qnyS5BQAJ> or my one <https://groups.google.com/g/metamath/c/91QTr-3TvN0>? Arguably, nearly all long-hanging fruit in the Metamath 100 list are done (besides, maybe some things related to geometry). People still look at that list, so it would be very useful in my opinion to break down the proof strategy into several steps and formalize *the statement* into Metamath (with empty proof). This can be placed in the set.mm github and tracked, for example, with an issue or a project, like Elementary Geometry and iset.mm do right now. -- 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/48ec5fe8-9733-4b96-a59c-5feee8a3137dn%40googlegroups.com.
