Stephen Wolfram has been investigating dependencies between theorems, including Metamath's set.mm, and has written up some findings here: https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/
He mentions that ~syl is the most popular set.mm theorem (as we know). It appears that ~syl isn't the most prominent in your propcalc.pdf; instead, I think ~id and ~a1i have the most arrows pointing to them. Apparently ~syl is mostly referenced after the prop calc section. Norm On Tuesday, November 10, 2020 at 6:00:03 PM UTC-5 Benoit wrote: > Hi all, > > I was tinkering with some visualizations of set.mm, and I thought those > two graphs could be of interest to some of you. They are the dependency > graphs among theorems of intuitionistic implicational calculus and of > propositional calculus using implication, negation and biconditional. In > other words, theorems up to ~loowoz and up to ~imim21b respectively. > > Benoît > > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/07bd5cb3-c844-4193-9d74-60c6ea7b4507n%40googlegroups.com.
