Mizar system
The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referred to and used in new articles.The system was created beginning in 1973 by Andrzej Trybulec and is being maintained at the University of Bialystok, Poland, at the University of Alberta, Canada, and at Shinshu University, Japan.
Mizar articles are written in ordinary ASCII. The Mizar language is close enough to the mathematical vernacular so that mathematicians can read and understand Mizar articles almost immediately; it is formal enough so that proofs can automatically be checked. All steps in a proof have to be justified, and it has been estimated that a Mizar article is about four times as long as an equivalent mathematical paper written in ordinary style.
The proof checker uses classical logic, is written in Pascal and can be downloaded and used for free for non-commercial purposes. It runs only on PC platformss, on Windows, Solaris and Linux. The source code is not available.
The Mizar distribution includes the Mizar Mathematical Library (MML) consisting of many definitions and theorems which can be referred to in newly written articles. These new articles, after having been reviewed and automatically checked, can be published in the associated Journal of Formalized Mathematics and then become part of the MML.
The MML is built on the axioms of the Tarski-Grothendieck set theory. As of 2003, it contained about 2000 definitions and 30,000 theorems. Examples are the Hahn-Banach theorem, König's lemma, facts about the Cantor set etc.
Even though semantically all objects MML talks about are sets, the language nevertheless allows to define and use syntactical types: a variable may for example be declared of type Nat if it stands for a natural number, or of type Group if it denotes a group. This makes the notation more convenient and closer to the way mathematicians think of symbols.
No easy browsing of the MML is implemented, and consequently one of the major problems facing a user of the system is to find out whether and where needed results are contained in the MML.
See also: QED project
External links
