Metamath

Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in logic, set theory, number theory, algebra, topology and analysis, among others. the set of proved theorems using Metamath is one of the largest bodies of formalized mathematics, containing in particular proofs of 74 of the 100 theorems of the "Formalizing 100 Theorems" challenge, making it fourth after HOL Light, Isabelle, and Coq, but before Mizar, ProofPower, Lean, Nqthm, ACL2, and Nuprl. There are at least 19 proof verifiers for databases that use the Metamath format. This project is the first one of its kind that allows for interactive browsing of its formalized theorems database in the form of an ordinary website. The Metamath language is a metalanguage, suitable for developing a wide variety of formal systems. The Metamath language has no specific logic embedded in it. Instead, it can simply be regarded as a way to prove that inference rules (asserted as axioms or proven later) can be applied. The largest database of proved theorems follows conventional ZFC set theory and classic logic, but other databases exist and others can be created. The Metamath language design is focused on simplicity; the language, employed to state the definitions, axioms, inference rules and theorems is only composed of a handful of keywords, and all the proofs are checked using one simple algorithm based on the substitution of variables (with optional provisos for what variables must remain distinct after a substitution is made). The set of symbols that can be used for constructing formulas is declared using $c (constant symbols) and$v (variable symbols) statements; for example: $( Declare the constant symbols we will use$) $c 0 + = -> ( ) term wff |-$. $( Declare the metavariables we will use$) $v t r s P Q$.