Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. Metamath lets you see mathematics developed in complete detail from first principles, with absolute rigor.