This is a site with Metamath tests. Metamath is a computer language used to express formal mathematics and other symbolic theories. Our tests are concentrated upon theory file. contains logic, set theory, number theory, group theory, algebra, analysis, etc. Milpgame is an application in which you can demonstrate a given statement using axioms and theorems and is based on Metamath.

Download, unzip and install Milpgame. Download .mm teory file ( and one of .mm test file(ex. and place them in the same directory(c:\Downloads). Open a test file(ex. with Milpgame and start to solve the problems. Milpgame must be used only with files from this site. 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
Beginning with Milpgame 0.3 you can save unfinished proofs in *.mlp format and you can open later to prove the theorem / problem.