Construct mathematics from basic axioms

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.

Command | Description |
---|---|

metamath | Formal proof verifier and proof assistant |