Instead, it can be regarded as a way to prove that inference rules (asserted as axioms or proven later) can be applied.

The largest database of proved theorems follows conventional first-order logic and ZFC set theory.

[8] The Metamath language design (employed to state the definitions, axioms, inference rules and theorems) is focused on simplicity.

This theorem would never appear under this cryptic form in a textbook but its literate formulation is banal: when two quantities are equal, one can replace one by the other in an operation.

[10] The Metamath website hosts several databases that store theorems derived from various axiomatic systems.

Most databases (.mm files) have an associated interface, called an "Explorer", which allows one to navigate the statements and proofs interactively on the website, in a user-friendly way.

[12] Thus, people interested in studying mathematics can use Metamath in connection with these books and verify that the proved assertions match the literature.

The Metamath Proof Explorer (with its database set.mm) instead uses a set of conventions that allow the use of natural deduction approaches within a Hilbert-style logic.

[14] Levien would like to implement a system where several people could collaborate and his work is emphasizing modularity and connection between small theories.

Mel O'Cat designed a system called Mmj2, which provides a graphic user interface for proof entry.

[17] The initial aim of Mel O'Cat was to allow the user to enter the proofs by simply typing the formulas and letting Mmj2 find the appropriate inference rules to connect them.

There is also a project by William Hale to add a graphical user interface to Metamath called Mmide.

[18] Paul Chapman in its turn is working on a new proof browser, which has highlighting that allows you to see the referenced theorem before and after the substitution was made.

Milpgame is a proof assistant and a checker (it shows a message only something gone wrong) with a graphic user interface for the Metamath language(set.mm), written by Filip Cernatescu, it is an open source(MIT License) Java application (cross-platform application: Window, Linux, Mac OS).

User can enter the demonstration(proof) in two modes : forward and backward relative to the statement to prove.

Milpgame is distributed as Java .jar(JRE version 6 update 24 written in NetBeans IDE).