On Tue, Nov 22, 2022 at 8:50 PM David A. Wheeler <
dwhe...@dwheeler.com> 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.