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.