My essay yesterday represents the opinion I formed after looking back and reflecting on some things I felt were accomplished successfully and others not so successfully with set.mm. I try to keep an open mind, and my opinion can change if I can be convinced another way is better.
Careful choice of definitions seems essential to the success of set.mm and its philosophy, and that is what I focused on. My purpose is not to dictate mandatory rules but to open up a discussion of what the philosophy should be, particularly with regard to definitions, using my suggested rules as a starting point and a possible guide. I didn't intend to diminish the value of anyone's work with the specific examples I brought up. If I was perceived as too critical I apologize for that. I simply used them as convenient illustrations for the discussion. And it is possible I am wrong. I appreciate the contributions made by everyone and recognize that it has involved serious, hard work with good intentions. In any case, the definitional "rules" didn't even exist before I wrote them down last night, so it's hardly fair to have expected anyone to have followed them. ---- As for goals for set.mm (as opposed to "philosophy"), coming up with a long-term master plan of some sort is difficult because people's interests vary widely. I would fear that vague things like "build an algebraic hierarchy" would end up as a voluminous collection of definitions without a lot of substance. Instead, I would prefer to see some significant theorems (such as named theorems in the literature) as goals, which for example might drive the creation of an appropriate algebraic hierarchy when it becomes essential to have it. We do have the MM100 list if we want some concrete targets, and anyone can focus on those (and make David, and me, very happy...). We might as well call those official goals. Curiously, if I type "list of named theorems" in Google, Freek's list (the MM100 list) appears at the top in a big box. So I guess Google thinks they're important. :) It certainly gives Metamath a lot of visibility, being in 3rd place. Anyway, the next link down is to the page https://en.wikipedia.org/wiki/List_of_theorems with a huge list with a thousand or more named theorems. So there are plenty to choose from. Personally, if a magic genie were to offer me a set.mm proof of any theorem I chose, I would probably pick FLT. (And I might as well exploit the genie's magic and ask for the shortest possible proof.) I don't know if it is realistic to consider FLT as a possible "flyspeck" (Kepler conjecture) type project, but the huge amount of background material that would have to be developed would be amazing and probably useful for many other things long before the final goal is reached (if it ever is). What would other people like to see (magic genie or not)? Norm On Thursday, January 23, 2020 at 11:58:14 PM UTC-5, Norman Megill wrote: > > Tierry, Alexander, and Benoit have asked for clarification of the goals of > set.mm. Here are some of my opinions. I am moving the discussion in > https://github.com/metamath/set.mm/issues/1431 to here for wider > readership. > > *.....* > -- 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/71f68dff-1393-4be1-9ffa-b0ca6f5768f3%40googlegroups.com.
