Mizar system

For the star system, see Mizar (star).

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 referenced and used in new articles. Mizar has goals similar to those of the QED project proposed by Bob Boyer around 1993. Mizar is proprietary.^[1]

History

The system was created beginning in 1973 by Andrzej Trybulec and is maintained at Białystok University, Poland, the 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 that mathematicians can read and understand Mizar articles almost immediately; it is formal enough that proofs can be checked automatically. 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 freely used for non-commercial purposes. It runs on PC platforms, Windows, Solaris, FreeBSD and Linux, and Mac OS X/Darwin. The source code is available only to members of the Association of Mizar Users.^[2]

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 checked automatically, can be published in the associated Journal of Formalized Mathematics^[3] and then become part of the MML.

The MML is built on the axioms of the Tarski-Grothendieck set theory. As of February 2010, it contained about 9500 definitions and 49,500 theorems.^[4] Examples are the Hahn–Banach theorem, König's lemma, Brouwer fixed point theorem, Gödel's completeness theorem, and facts about the Cantor set.

Even though semantically all objects MML talks about are sets, the language nevertheless allows one 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^[3] and MML Query^[5] implements a search engine for MML.

See also

• QED project
• Automath

References

1. ^ Mailing list discussion referring to the close-sourcing of Mizar.
2. ^ Association of Mizar Users
3. ^ ^{a b} Journal of Formalized Mathematics
4. ^ see [1] for up-to-date statistics
5. ^ MML Query (home page)

External links

• Main Mizar site, contains links to the MML, to the Journal of Formalized Mathematics, and a bibliography section linking to several introductions to the system
• MML Query, is a search engine for MML.
• Freek Wiedijk's Mizar site, contains slides of a conference talk about the system, as well as a 40 page introductory article
• Association of Mizar Users
• A paper about Mizar history (ps)
• A comparison between Mizar and another (Automath-like) formal language for mathematics, Weak Type Theory.
• Mizar wiki