Related: Metamath (http://www.metamath.org http://www.metamath.org) is a tiny formal language for writing proofs in symbolic logic, as well as a tiny proof chec

Related: Metamath (http://www.metamath.org http://www.metamath.org) is a tiny formal language for writing proofs in symbolic logic, as well as a tiny proof checker for the language. The author, Norm Megill, has used Metamath to formalize many theorems from set theory and analysis. For example, see his formalization of a typical proof that the square root of 2 is irrational: http://us.metamath.org/mpeuni/sqr2irr.html http://us.metamath.org/mpeuni/sqr2irr.html