Metamath is interesting for education in the principles of formal proofs, because:

1. The Metamath Book is self-contained well written, simple introduction.

2. Everything is explicit, nothing is hidden.

3. Because of extremely simple syntax and semantics it's easy write own proof verifier.

The drawbacks are:

1. Non-standard approach to free and bound variables.

2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.

3. Almost no proof automation. No tactics. Long, hard to read proofs.

I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.