-
Notifications
You must be signed in to change notification settings - Fork 89
Metamath Proof Assistants
Metamath databases (files that define axioms, theorems, and the proofs of theorems) are written in the Metamath file format. Such files are text files can be viewed and edited by any ASCII editor which can handle their size. The precise technical specification of the language is given in Section 4.1 (p. 92) of the Metamath book. However, individual proofs Metamath databases are usually compressed, and it requires a proof assistant to write one. In practice, it's much easier to create proofs using a tool to help you. The Metamath proof assistants most widely used today to create Metamath proofs are mmj2 and the original Metamath (metamath.exe) program:
MMJ2 is a java-based GUI Proof Assistant for the Metamath language. It includes thorough file validation and proof verification, syntactic parsing of Metamath formulas and many other features. With its GUI and automatic transformation features, it is the preferred way to edit longer and more complex proofs, however it does not work directly on the Metamath files, but on a specific "MMP" file format for metamath proofs, which then have to be imported in metamath files.
David A. Wheeler produced two introductory videos "Introduction to Metamath & mmj2" and "Creating Functions in Metamath".
mmj2 comes with a detailed hands-on tutorial in its documentation folder. If you like, you can watch a video walkthrough of the tutorial in mmj2. You can also see details on the now archived AsteroidMeta wiki.
See the main metamath page for more on MMJ2.
Metamath-lamp is a browser-based proof assistant similar to mmj2.
The proof assistant is available here, and a guide has been written for it. David A. Wheeler has produced introductory videos for Metamath-lamp, which are available here.
The Metamath program is an ASCII-based ANSI C program with a command-line interface. Along with building and verifying Metamath proofs, it can also be used to perform batch operations on proofs, reformat Metamath files, and generate web pages. Its command-line interface mode makes it rather difficult to build long and complex proofs, but it is still interesting to learn how e.g. substitutions work.
Detailed instructions on how to use the metamath program can be found in its HELP built-in command, specifically in HELP PROOF_ASSISTANT.
See the main metamath page for more on the Metamath program.