Sponsor:

Your company here — click to reach over 10,000 unique daily visitors

Package metamath

Construct mathematics from basic axioms

https://us.metamath.org/

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