Preface

Mizar is one of the most famous proof checkers. It is historically very old and also thought to be the most accurate for genuine mathematical language. There seem to be several types of proof checkers in the world; however, those were made by graduate students for their graduation thesis and many of them were abandoned once the students graduated. Because of this situation, Mizar's library is increasing with the help of the Mizar group lead by Prof. Andrzej Trybulec as well as many other researchers and graduate students.

Since Prof. Trybulec is a mathematician, he knows about what kinds of proof checkers are needed. Therefore, because these were made under such experiences, their functions are thought to be substantial. This proof checker was non-existent in the old days; therefore, mathematics were thought to be very rigid. Many people thought that dependence in machines were not necessary. However, corresponding with the development of computers, this rigidity became questionable. As a result, a question rose as to how mathematics should be written. Every proof checker has different ideas. My creation, THEAX, is one of them; however, it was totally independent from Mizar even though it was created about the same time or a little later than Mizar. Therefore, the way of thinking is entirely different.

Here, we would like to explain Mizar's way of thinking, the actual environment of movement, and the story about what kind of thinking made formalized mathematics.