This is a site that contains Metamath tests and a Java application:Milpgame. Metamath is a computer language used to express formal mathematics and other symbolic theories. Our tests are focused upon set.mm theory file. Set.mm contains logic, set theory, number theory, group theory, algebra, analysis, etc. Milpgame is a proof assistant and verifier in which you can demonstrate a given statement using axioms and theorems and is based on Metamath.


Download Milpgame0.4.zip, unzip and follow the instructions on readme.txt. For proving theorems on current set.mm, download set28.07.2017.mm and open the file with Milpgame. For playing with Metamath tests, download .mm teory file (set04.06.2013.mm) and one of .mm test file(ex. test1.mm), place them in the same directory(c:\Downloads), open a test file(ex. test1.mm) with Milpgame and start to solve the problems. System requirements: 2 GB of RAM and 1366x768 screen resolution. Use always the last available version of Milpgame.

Metamath tests:

If you like our tests we will make more for you! Good luck!
If you master Milpgame and/or Metamath you can send us via e-mail new Metamath tests with solutions, we will publish them!


HELP: Here we will present how the game works!

Video tutorial no. 1
Video tutorial no. 2
Starting with Milpgame 0.3 you can save unfinished proofs in *.mlp format and you can open later to prove the theorem / problem.
Starting with version 0.4 if you enter on Edit->Search and search for a theorem name you can go the source of theorem and thus you can enter new proof.