On Tue, Nov 22, 2022 at 8:50 PM David A. Wheeler <[email protected]> wrote: > > 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.
I think it is a great and important idea. As a greenhorn I have a fresh eye for this. Supposed that a student is already able to compile a simple proof, I think the most interesting property of Metamath for outsiders is that it gives constant theorem verification feedback for its users (plus all inputs and outputs of the transparent verification process are both human and machine readable). This means that (properly prepared and instructed) students are able to *experiment* with different proofs or even with different definitions (how would you define this; if you define it this or that way then what follows from them, what is and why exactly this is the definition of it in set.mm which accumulates explicit knowledge, etc.). For example, in the case of axioms, what a great piece of storytelling is the comments of https://us.metamath.org/mpeuni/ru.html ! Can we use this as a tool as an approach to introduction? Or what a context-revealing approach is the one in Appendix 7 https://us.metamath.org/mpeuni/mmset.html#subsys ! Of course I do not think that an introduction should begin with the comparison of the consequences of the alternate axiom/definition systems - perhaps, after the first steps, analysis/reproduction of some great theorems is the right way forward - but I feel that this constant feedback property opens up some exciting new ways for introduction into Meta/math. -- 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/CAJJTU5pe2QBU8%2Buf5LFTpp%2BzXrvVP%2B5DJNOkSXY0Lm32mGpNww%40mail.gmail.com.
