Guix

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, set.mm, 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.