Pedagogy
The method of proof used by Metamath is far different from what is used in a school context. In schools what is required is the literate, synthetic method of proof developed by mathematicians since Euclid's time. In Metamath, the method of proof is the symbolic, analytical method of proof invented by Aristotle, Leibniz, Peano and Frege. Thus, Metamath is unsuitable for school exercises. To speak simply, the proofs in Metamath are much too detailed to be used with ease in school. However, set.mm can be used in a school context as an example of a symbolic system that is big enough to be interesting. set.mm can also be useful because its detailed, symbolic, unambiguous definitions can resolve confusion with textbook definitions. Students may also appreciate the rigor of the Metamath Proof Explorer; no steps are skipped, no assumption left unstated, and no proofs are left "to the reader."
The Proof Explorer references many text books that can be used in conjunction with Metamath. Thus, people interested in studying mathematics can use Metamath in connection with these books.
Read more about this topic: Metamath