Mizar System
The Mizar system consists of a formal language to write mathematical definitions and proofs, a proof assistant that mechanically checks recorded in this language evidence, and a library of formalized mathematics, on which can be used in the proof of new theorems. The system is the Mizar Project, formerly under the leadership of its founder Andrzej Trybulec, maintain and further developed.
The Mizar Mathematical Library is the world's largest collection of strictly formalized mathematics.
- 3.1 width
- 3.2 Availability
- 3.3 Logical Structure
History
The Mizar Project was started in 1973 by Andrzej Trybulec in an attempt to reconstruct the mathematical jargon so that they can be checked by a computer. The current target, in addition to further development of the Mizar system, is the collaborative creation of a large library formally verified evidence which should cover the majority of modern mathematics. This is in keeping with the QED manifesto.
Currently, the project is managed and developed by research groups at the University of Białystok (Poland), the University of Alberta (Canada) and Shinshu University ( Japan). While the program is proprietary to test evidence, the Mizar Mathematical Library - licensed open -source - the library formally verified mathematics.
Papers relating to the Minzar system appear regularly in journals of the Academic Society of mathematical formalization. These include Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning and the Journal of Formalized Reasoning.
Name
According to the information from Andrzej Trybulec the double star Mizar is in the constellation of the great cars of the namesake of the project.
Mizar language
The outstanding feature of the Mizar language is its readability. As usual in mathematical texts, it is based on classical logic and declarative style. Mizar articles are written in ordinary ASCII, but the language was designed so that it is close enough to the mathematical jargon that most mathematicians can understand Mizar articles without special training. Nevertheless, the language allows a greater degree of formality required for the automatic test evidence.
This evidence is accepted, all steps must be justified, either with elementary logical arguments or citation already verifzierter evidence. This results in a higher level of detail than usual in ordinary mathematical textbooks and publications. Therefore, a typical Mizar article is about four times longer than an equivalent paper that was written in ordinary style.
The formalization of a theorem in the Mizar language is relatively labor intensive, difficult but not impossible. Once one is familiar with the system, it takes about a week of full-time work in order to be verified a text book page formal. This suggests that the benefits of the system in range of applied areas such as probability theory and economy.
Mizar Mathematical Library
The Mizar Mathematical Library ( MML ) contains all the theorems, which may relate to new products. Once items are akzekptiert the proof auditors, they are further reviewed externally and studied style and value of the contribution. If they are accepted, they will be published in the Journal of Formalized Mathematics own and added to the MML.
Width
In July 2012, the MML comprised 1,150 articles written by 241 authors .. Together these comprise more than 10,000 formal definitions of mathematical objects and about 52,000 proven theorems about these objects. More than 180 named math facts were formally coded. Examples are the Hahn- Banach theorem, the lemma of King, the fixed point theorem of Brouwer, of Gödel's completeness theorem and the Jordan curve theorem.
The breadth of coverage led some people to suggest he Mizar as a leading approximations to the QED Manifesto, the Kodiereung all of mathematics in computer verifiable form.
Availability
The query website implements a powerful search engine for the content of the MML. Among other things, it can all MML theorems that have been proved beyond a certain type or operator list.
Logical Structure
The MML is based on the axioms of Tarski - Grothendieck set theory. Although all objects are semantically quantities, allows the language the definition and use of weak types. For example, an amount only be declared as type Nat, when its internal structure with a specific list of requirements is compliant. In turn, this list serves as a definition of the natural numbers and the set of all sets that are compliant with this list is referred to as NAT. This implementation of the types tried the way as the most mathematicians reflect thinking about symbols and thus make the process of codification easier.
Mizar Proof Checker
Distributions of the Mizar proof checker for common operating systems are freely available for download from the Minzar website. The use of the proof chekers is free for non- commercial applications. The software was written in Free Pascal, and the source code is available for all of the Association of Mizar Users Members.