On Saturday, January 25, 2020 at 5:10:21 PM UTC-5, Alexander van der Vekens wrote: > > On Saturday, January 25, 2020 at 3:12:17 PM UTC+1, David A. Wheeler wrote: >> >> Giovanni Mascellani: >> > To me MM100 is a an interesting goal, but definitely an intermediate >> > one. The (admittedly, very ambitious) goal that I have in mind for >> > Metamath (or MM0, or whatever incarnation of it we will have in the >> > future) is that virtually every published mathematical result is >> > available in set.mm or some reverse dependency of it. I envision that >> if >> > you search for the comment "(Based on ArXiv paper: xxx.yyy)" you find >> > all the main theorems from that ArXiv paper. >> >> My goal is similar. I would like to see a future descendent of Metamath >> databases (including set.mm and iset.mm) >> have essentially *all* mathematics formalized. >> >> > I want to associate myself with Giovanni and David: the goal should be a > database in which "every published mathematical result is available" and > which has "essentially *all* mathematics formalized". >
This is a great goal and we can dream it, but it won't happen for decades or a century or maybe never. In the meantime, what is the first step? What specifically should people work on now? Perhaps we should look at what we would like to achieve in say 1 year, 2 years, 5 years. Of course people will want to work on what interests them, but having specific and realistic goals to select from might be useful to guide them. While the MM100 list is simply someone's opinion of important theorems, I was surprised at how visible it is (with Freek's list at the top of the Google search for "list of named theorems"), and it is definitely publicity for Metamath. A few years ago Metamath was rarely noticed by anyone in the field, whereas more and more I see it mentioned in slide presentations and article references. The more people who are aware of Metamath, the more contributors we will probably have, moving faster towards "all of mathematics". In 2016 I wrote on this newsgroup, "...by far the most important part of the Metamath project is not the language but the proofs people have contributed. While it is interesting to speculate how Metamath might evolve in 100 years with advances in computer technology, proofs that I formalize now will, in some form, live on forever as a foundation that will be built upon and always have my name associated with it. They are permanent. This contrasts to almost everything else in the software world, which with few exceptions become obsolete and forgotten in a decade or two..." Whether or not that will turn out to be true, believing it gives me a great deal of satisfaction and keeps me inspired. Already with MM0 and its translators to Lean and others, we are close to a point where "my" proofs (and yours) may become important in other proof languages as well. ... > Concerning simplicity, however, a knowledge base containing much/most of > mathematics cannot be simple in general, because mathematics is not simple. > But to use this knowledge base can (and should) be *made* simple by > providing appropriate tools and "views". Because of this, there could be > complex definitions in set.mm. Actually there are a lot of them, which > only become clear by the corresponding "defining theorems" - e.g. > ~df-mamu: > $a |- maMul = ( r e. _V , o e. _V |-> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( > 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( > m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> > ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) ) $. > which becomes clear only after looking at theorem ~mamuval: > $p |- ( ph -> ( X F Y ) = ( i e. M , k e. P |-> ( R gsum ( j e. N |-> ( ( > i X j ) .x. ( j Y k ) ) ) ) ) ) with F = ( R maMul <. M , N , P >. ) > I agree that ~ df-mamu (and ~ mamuval for its practical use) is a good example. In particular, it is used directly or indirectly by 224 theorems, so there is no question that it is useful and even essential. BTW it would be a good idea to reference ~ mamuval in the description of df-mamu. We often do that for value theorems (or at least I have done so in e.g. ~ df-re). df-mamu illustrates another point. If we look at the reference cited (Lang p. 504), the actual form of df-mamu cannot easily be deduced from the definition printed on that page (a mixture of informal language and some formulas). My guess is that df-mamu was need-driven (its author S.O. would have to answer that) i.e. was added as the theorems needing it were being proved and it was needed to move forward. It likely required an intimate knowledge of how it was going to be applied along with knowledge of the set.mm objects it was going to be applied to. Thus I think it is unlikely that someone simply transcribing definitions from a book would come up with exactly df-mamu. In addition, while I don't know the history of df-mamu specifically, my own experience is that I've often had to fine-tune complex definitions to achieve what I wanted from them. Sometimes problems can be determined only by actually using the definition in its intended application. I know I keep harping on not wanting to add a catalog of definitions (with shallow theorems) that are otherwise unused, but it has been done in the past with the work essentially wasted, sometimes causing resentment, and I want to avoid that. With an ambitious goal like "all of mathematics," it will be very tempting to start collecting definitions, leading to a false sense of accomplishment to see the syntax errors ironed out and simple property theorems proved. But in the end it is busywork with a good chance of being discarded later. Moreover, a few shallow value and property theorems don't ensure that the definition is correct, possibly misleading someone who might want to use set.mm as a reference source that can be trusted to be rigorously correct. This is the motivation for rule 2 I proposed, "definitions shouldn't be introduced unless there is an actual need in the work at hand." One thing I have done in the past is to add definitions I expect to use eventually in commented-out form, in order to serve as a reference to help guide the project's direction. When they become needed, I uncomment and adjust them based on how the project and its notation actually evolved. Quite often definitions not in the literature will be needed to help fill in gaps in the informal proof. Other times definitions in the literature end up not being useful or have to be modified for the needs of the formalization. We have to remember that authors of written proofs are human, they usually have no idea their work will be formalized nor appreciate what kind of definitions are needed for that, and they may gloss over edge cases and other details that affect a rigorous formalization. Norm > By providing tools and views, the underlying data/knowledge base can be > used by non-specialists (using simple views) as well as by experts (using > advanced views). > > On the other hand, if set.mm is used as library (or tool box) to provide > and prove new theorems, it is also very helpful if it is complete as > possible: I do not want to provide hundreds of auxiliary theorems first, I > expect that they (or at least most of them) are simply there (OK, this is a > vision, but we should work on it). If set.mm becomes too big to find the > adequate theorems easily, the tools and views need to be improved. But this > is again not a problem of the data/knowledge base. > > To conclude: To answer the question about the goals for set.mm, we have > to agree on the purposes (e.g. knowledge base/library vs. pedagocial > textbook) and the properties (completeness, beauty, simplicity, brevity, > etc.) first. > > -- Alexander > > -- 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/dbdd5f3e-452c-4f46-a1ca-e80087a2d6da%40googlegroups.com.
