I'm definitely not a regular contributor to set.mm, yet the topic discussed is so interesting that I would like to comment on it.
I think defining the "goal of set.mm" is of little use, since goals must be achievable and things like "formalize all of mathematics" imply that either mathematics will cease to develop or all created mathematics will somehow find place in set.mm which doesn't sound very realistic. We don't see software libraries containing all possible functions and procedures or mathematical treatises covering the whole of mathematics (even "Elements of mathematics" don't come close), so in my opinion neither should set.mm try to formalize the whole body of mathematical knowledge. I personally would like to see set.mm as an attempt to formalize "standard" mathematics, to form a mathematical "core library" which can be used to leverage the formalization of other fields. It is mostly old mathematics for sure, but even formalizing basics of algebra, analysis, topology, geometry etc. looks like a worthwhile goal for set.mm. I think the Metamath 100 list serves as a good guide to which topics should be covered and right now it is still a stable source of feasible tasks for formalization. I don't remember if this has been suggested before, but we could also form our own, say, "Metamath 200" list which will contain other results metamath community deems important. As for moving contributions to the main part, I fully support the "move when used by someone else" strategy. As Alexander demonstrated, it is hard to judge whether something is "serious" or "important" without being subjective, so probably strict rules like "move on use" are more preferable. Recently it was agreed that Metamath 100 results are also important enough to be moved into the main part, and I think these rules are explicit enough to reduce any disputable judgements to a minimum. There are certain cases when "big" results are moved into the main part as an exception from mentioned rules. Since such cases seem to generate much discussion, maybe those rules should be enforced in all cases? That might slow down the accumulation of results in the main part, but at least it will be fair to everyone. Another solution would be to follow a fixed set of books (say, Bourbaki), since it will automatically solve the problem of structuring sections, choosing definitions and determining which results belong to the main part (I think FL suggested that before). I don't think it is that easy to pull that off in practice, for instance, many definitions in set.mm are tweaked to fit formalization needs (so they don't look like their mathematical counterparts). I still think the idea is important, and maybe we could adapt it in a modified way. Say, we prescribe a set of books to each section (for example, Lang to abstract algebra, Munkres to general topology etc), we try to structure these sections according to the book chosen and we import results to the main part if they match some theorem/proposition/etc from the book. That still leaves the question of how all definitions coming from the chosen book should be formalized in set.mm, but at least it puts the burden of deciding whether something is useful on the book author :-) Finally, I would like to comment on David's catalogue of definitions. Maybe instead of moving it to the end of set.mm and adding "discouraged" tags, it could be a separate database importing set.mm? It seems like the goal of cataloguing widely used symbols is not essential to set.mm, so keeping the unused definitions list in the main database is unnecessary. But, the catalogue could be a nice project by itself, which could benefit from being a separate database (for instance, one can use a completely different sectioning, say, alphabetical resembling a handbook). Also it might be one of the first good cases for using database imports. -- 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/3c9ffbe3-a29e-4868-8ded-e7379abb4b85%40googlegroups.com.
