On Saturday, September 5, 2020 at 11:56:58 PM UTC+2 Norman Megill wrote: > On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der > Vekens wrote: > >> That's sound really great! I will try this new feature soon, using the >> friendship theorem as "root"... >> > > Good choice. I was curious so I added it (temporarily) here: > > http://us2.metamath.org/ocat/friendship/mmtheorems.html > > Who would have known that it depends on Stoic logic? :) > Really impressive: so the friendship theorem depends on about 6500 theorems (of about 25000 in main set.mm, that is about one fourth!). And it depends only on about 300 theorems about graph theory itself. It will be exiting to analyse these dependencies in more detail...
> > I wrote about something similar that included the /extract functionality > (but with a much more ambitious goal in mind) in 2014: > > https://groups.google.com/g/metamath/c/hrtD9_wAcHM/m/fHL85-Hx5usJ > > set.mm was put on GitHub about 6 months later, addressing some of the > issues I brought up, and the idea of extract/merge was put on hold. But > I've always felt /extract could provide insight about a particular theorem, > and if nothing else would give you an idea of what background you need to > understand it fully. > > Norm > > -- 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/49f603d8-3a13-44fc-b05a-fb5540a0c4e8n%40googlegroups.com.
