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". And this database is (currently) set.mm, and it should remain set.mm (maybe not physically, e.g. as a single file, but logically, concerning its contents). Having this goal, set.mm is a knowledge base and a library: on the one hand to be read by interested people, who should find everything they are looking for (regarding mathematics, of course) and be confident that it is (formally) correct what they find (yes, they should also find a formal definition of a magma, and theorems which only uses the properties of a magma, asking themselves the question: do I really need an identity element to prove this?). Metamath (language and tools) provides an excellent basis for that (and this topic is not about the goal of Metamath, which is pretty clear and beyond all possible doubt - it's about the goal of *set.mm* and how to continue to improve/expand it).
To summarize this aspect, Giovanni, David and I request the following property of the database set.mm: Completeness (as far as possible)! Another property would be "Beauty" (see also section 1.1.4 in the metamath book): Not only the proofs should be beautiful (being short, elegant, tricky, etc.), but also the definitions and theorems themselves. And concerning the entirety of the database, its structure should also be beautiful! The properties "Simplicity" and "Rigor" (see also sections 1.1.5 and 1.1.6 in the metamath book) are "inherited" from Metamath (and the axioms provided within set.mm), so we do not need to question that. 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 >. ) 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/5ca4ef1e-adf9-4530-92ca-b3db13cfe69c%40googlegroups.com.
