On Saturday, January 25, 2020 at 5:10:21 PM UTC-5, Alexander van der Vekens wrote: > > the goal should be a > > database in which "every published mathematical result is available" and > > which has "essentially *all* mathematics formalized".
On Sat, 25 Jan 2020 18:40:53 -0800 (PST), Norman Megill wrote: > 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? ... 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". I completely agree. I think goals that are achievable in the "more near term" are very valuable. I think the MM100 list has given Metamath a lot of visibility AND it's encouraged development of a lot of intermediate theorems that are important and useful elsewhere. > 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. I think that as the set of proofs in Metamath increases, the likelihood of it continuing to grow increases. It isn't a big deal to create a few small proofs. But as more and more proofs are added to the database, anyone else who wants to formalize mathematics will be attracted to building on that database instead of starting from scratch. The Metamath language may change, or the databases may get translated into some newer system (like MM0), but that means the proof work endures. --- 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/E1ivZ0n-0007pm-0K%40rmmprod07.runbox.
