Created by Filip Cernatescu

[Added by NM 8-Mar-2018: The current version of Milpgame (0.5) has a 14-minute start-up time with, making it impractical for normal use. Filip says he will address this problem. In the meantime, it can be used for smaller databases.]

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, unzip and follow the instructions on readme.txt. For proving theorems on current, download the from Github/ 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

Source code

The program is released under the MIT license on Github [retrieved 28-Feb-2018].
  This page was last updated on 8-Mar-2018.
Copyright terms (for the text on this web page): Public domain
W3C HTML validation [external]