metamath

The metamath program is an ASCII-based ANSI C program with a command-line interface. It was used (along with mmj2) to build and verify the proofs in the Metamath Proof Explorer, and it generated its web pages. The *.mm ASCII databases (set.mm and others) are also included in this derivation.