I think we should not put everything in set.mm repo, or if we do, we clearly separate set.mm from the rest of it. I think there is already too much stuff in the repo that isn't about set.mm itself. What you have described clearly sounds like a separate project, like a blog post series or something, and as such it wouldn't need to stay rigidly in sync and could just pin a version of set.mm to work with.
On Tue, Nov 22, 2022 at 3:50 PM David A. Wheeler <[email protected]> wrote: > > I am trying to learn advanced math with assistance of Metamath. > > Cool! > > > I understand a lot of elementary theorems that are in the database. > However, I thought I would jump to (sqrt2irr -Irrationality of square root > of 2), but its proof isn't really making sense to me. > > I've toyed with the idea of creating an "Introduction to Formalized > Mathematics Using the Metamath Proof Explorer (MPE)". > It would highlight the key axioms, definitions, and proofs (with links), > with an idea of creating a simple > introduction to the idea & how it's done in MPE. It might be gentler "way > to start" > instead of reading MPE directly. It could be done in a different > repository, but > if it was in the same repository it'd be easier to keep consistent. > > I'd be curious if anyone else thought it'd be a good idea. > > --- 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/46339806-74AD-42C1-B8C3-787454AB0708%40dwheeler.com > . > -- 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/CAFXXJSsC9WsVjo8zPEH57WXEpTZ1bamsDF57BcjhEsUrsm44vw%40mail.gmail.com.
