> > I think we should try to curate a small selection of set.mm propositional > logic and predicate logic, enough so that you have all the main theorems > but not going for absolute saturation, with interstitial "tutorial" > comments explaining the anatomy of an mm file along the way. >
Exactly. Look at Kevin Buzzard's natural number game along these lines - that's the best introduction to Lean's tactical framework. But you should have known it already. BTW, according to Thurston's paper cited in that Buzzard's blog, the best way to disseminate mathematical knowledge is from first-hand experience. -- 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/b1a3a4c7-366e-4dc6-9ee4-099d82f7d47e%40googlegroups.com.
