Package metamath
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 |