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.