Metamath is a simple and flexible computer-processable language that supports rigorously verifying, archiving, and presenting mathematical proofs. See the FAQ for more information. Metamath Proof Explorer - Constructs mathematics from scratch, starting from ZFC set theory axioms. Over 23,000 proofs. Theorem list Recent proofs (this mirror) Intuitionistic Logic Explorer - Derives mathematics from a