Introduction


Traditionally, mathematics has been the most strict subject. However, it is questionable if it is really rigorous like it has been said because the method of describing mathematics accurately is not established and objective way of checking correctness of the proof is not given; therefore, there is no way to avoid subjectivity of mathematicians or groups. Because of this, the education of mathematics had to convey tacit promises from mentors to pupils and this basically made the world of mathematics exclusive. The fist evil is the declining numbers of people who can understand certain fields of mathematics and because of this, the power of influencing other fields of study seems to be corroding. Secondly, even though mathematics is a free subject, when the new theory is too original, there is an inclining danger of abandoned work due to difficulty of acquiring people who can read and understand it or have time to do so. Thirdly and this should be the biggest reason, when the production of computers and the number of computer users get increased, it seems that the strictness of basic mathematics becomes rocky. The strictness of the computer language is to the point where existence of one period matters and logically, among millions of steps, there is not even a single logical mistake. The reason why the program language cannot be replaced for mathematics is simply because its expression ability is not enough compared to mathematics.

Therefore, I will introduce the way of normal mathematical language that is inputable to computers and improvement that automatically checks for mistakes in the written proof after the restoration. In the process of making this system, careful attention was paid to using daily language as much as possible and so to speak, set a target to practical language and its arrangement. However, compare to natural language with symbols used by mathematicians, it may still be inaccessible. Nevertheless, I believe that it is much more practical compare to Principia Mathematica by Russel and Whitehead. Moreover, for young people who are familiar with computer languages, it is possible that our clearly explained language is easier to understand. This system is also educationally good for making young people clearly and experientially (by using such as conversational terminal) comprehend what mathematics is. In fact, we are testing its effect on students in information mathematics classes of the department of information engineering in Shinshu University for several years, and their ability of perception is above expectation. In addition, they seem to enjoy this system and joy of getting the indication of " Proof is complete" for their own proof is exceptional.

There can be criticisms for taking such ways. Mathematicians probably will consider this as a wrong way for mathematics. They may insist on saying that mathematics is not a formality and the importance is in the contents. However, considering this critique, if there are physicists with great ideas, there might be no need for mathematicians. Also, traditional way of writing is superior in sketching the course of proofs and it can be compatible with our strict way of writing. On the other hand, computer scholars may disapprove from different view points. That is, for demonstrations, this is the time of letting computers do it automatically, and this system that only checks the rightness of proofs is slow in development. We also think that automatic demonstration is hopeful. However, except for very elementary parts, mathematics in reality is far from becoming able to do so. Our trial is the first step towards that and it is not denying complete automation.

Because we were headed for its practicality, this system named THEAX (Theory Automatic Checker) in some cases has sacrificed grammar and its concise interpretation way. That way of writing or reasoning have been acquired in the traditional mathematics' long history of learning and they cannot be arbitrarily disproved at this point. Nevertheless, taking this system as an opportunity, whether those are right or wrong maybe discussed. If we are able to acquire consent from most mathematicians, terser construction of the system will not be impossible. Despite of sacrificing little condensation, this system can also point out the basic problems that were usually not noticed by mathematicians. For example, concerning natural number theory, the reason that makes it possible to inductively define functions that are in the range of definition cannot be acquired from induction of axiom. Inductive axiom does not guarantee the existance of a function.

If it is permitted to state the later direction of THEAX, one is to be widely utilized for students' mathematical education. Also for students majoring in mathematics, even though they will use traditional mathematical language in the future, they will need to acknowledge the structure of scrupulous mathematics once, so at some point, rewrite with THEAX and then data base it. Moreover, it will be wonderful if new mathematics that is written with THEAX gets reproduced. Traditionally, research for mathematics tended to be closed; however, it will be possible to open it up widely to amateurs. Because there is no need to check demonstrations, judgment of research papers will speed up and if there are second Evariste Galois or Niels Henrik Arbels, it will be easy to discover them (for that, publicized unsolved problems will be helpful). Other direction is by placing THEAX as a base, make more concise language without been tied up by the practicability. That should be helpful for researching the basic mathematics more deeply. In addition, there is a possibility of THEAX being useful for designing systems for software. Thus, mathematics has a better ability of expression than computer language, and because of this, an ability to describe general systems seems to be greater.