Mizar system
From Wikipedia, the free encyclopedia
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. Mizar has goals similar to those of the QED project proposed by Bob Boyer around 1993.
Contents |
[edit] 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 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 and non-commercial purposes. It runs on PC platforms, Windows, Solaris, FreeBSD and Linux, and Mac OS X/Darwin. The source code is only available to members of the Association of Mizar Users.[1]
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[2] and then become part of the MML.
The MML is built on the axioms of the Tarski-Grothendieck set theory. As of March 2008, it contained about 8800 definitions and 46,000 theorems.[3] 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 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[4] and MML Query[5] implements a search engine for MML.
[edit] See also
[edit] References
- ^ Association of Mizar Users
- ^ Journal of Formalized Mathematics
- ^ see [1] for up-to-date statistics
- ^ Journal of Formalized Mathematics
- ^ MML Query (home page)
[edit] 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
