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, University of Alberta, Canada, and 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 on PC platforms, Windows, Solaris, FreeBSD and Linux, and Mac OS X/Apple Darwin. The source code is only available to members of the Association of Mizar Users (http://mizar.uwb.edu.pl/sum/).
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 2005, it contained about 8000 definitions and 40,000 theorems (see [1] (http://merak.pb.bialystok.pl) for up-to-date statistics) . Examples are the Hahn-Banach theorem, König's lemma, Brouwer fixed point theorem, Gödel's completeness theorem, 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.
Browsable abstracts of MML articles are available as the Journal of Formalized Mathematics (http://mizar.uwb.edu.pl/JFM/), and MML Query (http://merak.pb.bialystok.pl) implements a search engine for MML.
See also
External links
- Main Mizar site (http://www.mizar.org), contains links to the MML, to the Journal of Formalized Mathematics, and a bibliography section linking to several introductions to the system
- MML Query (http://merak.pb.bialystok.pl), is a search engine for MML.
- Freek Wiedijk's Mizar site (http://www.cs.kun.nl/~freek/mizar/), contains slides of a conference talk about the system, as well as a 40 page introductory article
- Association of Mizar Users (http://mizar.uwb.edu.pl/sum/)
- A paper about Mizar history (http://merak.pb.bialystok.pl/mkm2004/RMatuszewskiPRudnicki.ps)