# Metamath Proof Explorer

We are sad to report the passing of Metamath creator and long-time contributor Norm Megill (1950 - 2021).

Norm of course was the author of the Metamath proof language, the specification, all of the early tools (and some of the later ones), and the foundational work in logic and set theory for set.mm.

His tools, now at https://github.com/metamath/metamath-exe , include a proof verifier, a proof assistant, a proof minimizer, style checking and reformatting, and tools for searching and displaying proofs.

One of his key insights was that formal proofs can exist not only to be verified by computers, but also to be read by humans. Both the specification of the proof format (which stores full proofs, as opposed to the proof templates used by most proof assistants) and the generated web display of Metamath proofs, one of its distinctive features, contribute to this double objective.

Metamath innovated both by using a very simple substitution rule (and then using that to build more complicated notions like free and bound variables) and also by taking the axiom schemas found in many theories and taking them to the next level - by making all axioms, theorems and proofs operate in terms of schemas.

Not content to create Metamath for his own amusement, he also published it for the world and encouraged the development of a community of people who contributed to it and created their own tools. He was an active participant in the Metamath mailing list and other forums until days before his passing.

It is often our custom to supply a quote from someone memorialized in a mathbox entry. And it is difficult to select a quote for someone who has written so much about Metamath over the years. But here is one quote from the Metamath web page which illustrates not just his clear thinking about what Metamath can and cannot do but also his desire to encourage students at all levels:

Q: Will Metamath help me learn abstract mathematics? A: Yes, but probably not by itself. In order to follow a proof in an advanced math textbook, you may need to know prerequisites that could take years to learn. Some people find this frustrating. In contrast, Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically. You can actually jump in anywhere and be convinced that the symbol string you see in a proof step is a consequence of the symbol strings in the earlier steps that it references, even if you don't understand what the symbols mean. But this is quite different from understanding the meaning of the math that results. Metamath alone probably will not give you an intuitive feel for abstract math, in the same way it can be hard to grasp a large computer program just by reading its source code, even though you may understand each individual instruction. However, the Bibliographic Cross-Reference lets you compare informal proofs in math textbooks and see all the implicit missing details "left to the reader."

1. Predicate calculus with equality: Older axiomatization (1 rule, 14 schemes)
2. Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16
3. Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old
4. Legacy theorems using obsolete axioms
5. Experiments with weak deduction theorem
6. Miscellanea
7. Atoms, hyperplanes, and covering in a left vector space (or module)
8. Functionals and kernels of a left vector space (or module)
9. Opposite rings and dual vector spaces
10. Ortholattices and orthomodular lattices
11. Atomic lattices with covering property
12. Hilbert lattices
13. Projective geometries based on Hilbert lattices
14. Construction of a vector space from a Hilbert lattice
15. Construction of involution and inner product from a Hilbert lattice