**Created by Filip Cernatescu**

Milpgame is a proof assistant and a checker (showing an error message
if something goes wrong) for the Metamath language. You can enter the
demonstration (proof) either forward and backward relative to the
statement to prove. Milpgame checks if a statement is well formed (the
program has a syntactic verifier). You can save unfinished proofs
without the use of the dummylink theorem. The demonstration is shown as a
tree, and statements are shown using HTML definitions (defined in the $t
typesetting comment of the database). Milpgame is distributed as a Java
.jar (JRE version 6 update 24 written in NetBeans IDE).

#### The following videos show how the application
works

Video tutorial no. 1
[retrieved 28-Feb-2018]

Video
tutorial no. 2 [retrieved 28-Feb-2018]
You can save unfinished proofs in *.mlp format, which
you can open later to complete the proof of the theorem or problem.

If you
enter on Edit->Search and search for a theorem name you can go to the
source of theorem and thus you can enter new proof.

Download Milpgame0.5.zip, unzip and follow the instructions on
readme.txt. For proving theorems on current set.mm, download the set.mm
from
Github/set.mm and open the file with Milpgame. System requirements:
2 GB of RAM and 1366x768 screen resolution.

For help
and feedback send Filip an email at
milpgame@yahoo.com

#### Source code

The program is released under the MIT license on Github [retrieved 28-Feb-2018].
Although it is primarily intended as a proof assistant, Milpgame can
also verify the full database in about 14 minutes (for set.mm). This
is not currently automated with a menu item, but it can be
performed by looping the function generateDemonstration located at line
3346 of
https://github.com/milpgame/milpgame/blob/master/project/src/spv/Source.java.
(This function is invoked each time a theorem is read by the
program.)