> 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.
