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 would like to see that for at least two reasons: 1. Provide *far* more confidence that what we think is true (given the axioms) is actually true. Mathematics is full of "proofs" that weren't, and as mathematics has become more complex, depending on humans to be perfect is becoming unjustifiable. There are other tools that have a lot going for them; I'll note that I like Coq. However, in most alternatives you never see what I call the "actual proofs"; you only see assertions that a tool thinks it found the actual proofs. Metamath is nearly unique in its focus that "every step must be visibly justified by a previous step", and that is what draws me strongly to Metamath. 2. Provide a stable archive of this information for all future time. I don't think people appreciate how ephemeral information is. The main logic system of the western world for centuries was Stoic logic; we know very little about it, because practically everything has been lost since. Modern civilization is even *less* good at archiving; most storage devices only last around 10 years, not thousands. Yet many civilizations have collapsed over the centuries, and it is hubris to think it could not happen again. I want to see etched copies of these databases put in caves, deep in the sea, on the moon, and sent out to space so it's possible for others to recover them after much else is lost. There are organizations like the Arch Mission Foundation (a non-profit organization that archives the knowledge and species of Earth for future generations, https://www.archmission.org/ ) - but they have to have material to work with. The Metamath 100 is merely an intermediate goal from this perspective, but I think it's useful. "Everything" is hard to achieve, while hard but more achievable & measurable goals is useful. (Fermat's Last Theorem probably won't be formalized for a while, but that's okay. What's a heaven for?) I think different people will have different goals. That is normal and expected. Hopefully we can find ways to work together; I think we can, because much has been accomplished so far. I intend to post more on this later, but other duties call for now :-). --- David A. Wheeler -- 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/E1ivMAa-0006bI-5Z%40rmmprod07.runbox.
