A proof checker consists of "a system of language for mathematics" and "a program to check the proof written in such a language". In many cases, a proof checker has a library which contains all papers written before and already checked their correctness. Users write their mathematical theories by such a fomal language, using some text editor(like MultiEditor). A text file written by such a way is called an article. A checker program checks its correctness automatically.

As such a proof checker, many are known. We have made an original proof checker called THEAX, an introductory text book of which is presented here.

At the same time, we will introduce another proof checker called Mizar, which was developed in Warsaw university (Bialystok branch). We are helping to enrich its library, because mathematics is universal, although each proof checker is different. We will give a lecture note for beginners of Mizar, and some useful links to other Mizar pages.

Download THEAX system for DOS(zip file)