This is a site that contains Metamath tests and an open source Java application:Milpgame(source code is available on Github/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 a checker (it shows a message only something gone wrong) for the Metamath language.You can enter the demonstration(proof) in two modes : forward and backward relative to the statement to prove. Milpgame checks if a statement is well formed(has a syntactic verifier).You can save unfinished proofs without the use of dummylink theorem. The demonstration is shown as tree,the statements are shown using html definitions (defined in typesetting chapter).Milpgame is distributed as Java .jar(JRE version 6 update 24 written in NetBeans IDE),in the near future I hope that will be available also on metamath.org site.


Download Milpgame0.7.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. 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 to the source of theorem and thus you can enter new proof.