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.

Version: 0.198

## General Commands | |

metamath | Formal proof verifier and proof assistant |