metamath 0.193 Proof verifier based on a minimalistic formalism

Metamath is a tiny formal language and that can express theorems in abstract mathematics, with an accompyaning metamath executable that verifies databases of these proofs. There is a public database,, implementing first-order logic and Zermelo-Frenkel set theory with Choice, along with a large swath of associated, high-level theorems, e.g.: the fundamental theorem of arithmetic, the Cauchy-Schwarz inequality, Stirling's formula, etc. See the Metamath book.