| Use computer to prove mathematical problem is a hot field which many countriesare taking active part in. Until now, there are many kinds of machine language systemwhich are use to prove mathematical theorems, and several of them are recognized bythe mathematician and computer experts, such as HO1, Mizar, PVS, coq etc. Thespecific goals of these projects vary. However, they have one common feature: thehuman writes mathematical texts and the machine verifies their correctness. Theproject Mizar started 30 years ago under the leadership of Andrzej Trybulec at thePlock Scientific Society, Poland. Since then, however, Mizar the process has evolvedto a proof checker with the largest known repository of formally verified mathematicalknowledge covering a number of topics. It also apples in many fields such asautocontrol, voice, image identification etc, and set a good foundation to mathematicsand the related major.In this paper, we describe the history of Mizar system and the method to use theMizar system. Then we give the definition of quaternion numbers, module, algebrastructre etc, and then we prove its properties. They have been checked by Mizarsystem, published in the journal of《Formalized Mathematics》system, and acceptedinto the MML.In this field, I have published 5 articles in the journal of《FormalizedMathematics》in the instruction of my tutor, please look at the page of 70. |
PDF Full Text Request