Hi, I have not been contributing anything for quite some time, so far from me to dictate what Metamath's goals should be, but since one of the reasons I like this place is that experienced people always seem supportive and interested into beginners' ideas, I'll share my thoughts.
Il 25/01/20 04:29, Norman Megill ha scritto: > 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. 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. (a requisite for this to happen, of course, is that tools for formalizing theorems become much much more powerful in terms of reducing the De Bruijn constant; interesting results are already appearing on this list, but we have a long way to go) > 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). My usual approach with wish-bounded genies is instead to ask for wishes that are as complex as possible, so that I can pack as much wishable material in them as possible. For example, I would rather ask for a proof of FLT that is much much longer than it needs to be, hoping that at some point there is also a proof of Poincaré's conjecture (possibly discarded with a dummylink, unless Poincaré's conjecture is actually a useful step in proving FLT, which would make it even more interesting). Next genie I find, I'll tell you if it worked. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/f4d215bc-25c7-6c17-e23b-e1828b3be9f1%40gmail.com.
signature.asc
Description: OpenPGP digital signature
