Mizar system
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems.[1] The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.
For the star system, see Mizar (star).In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.[2]
History[edit]
The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct mathematical vernacular so it can be checked by a computer.[3] Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics. This is in line with the influential QED manifesto.[4]
Currently the project is developed and maintained by research groups at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan. While the Mizar proof checker remains proprietary,[5] the Mizar Mathematical Library—the sizable body of formalized mathematics that it verified—is licensed open-source.[6]
Papers related to the Mizar system regularly appear in the peer-reviewed journals of the mathematic formalization academic community. These include Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning and the Journal of Formalized Reasoning.
Mizar language[edit]
The distinctive feature of the Mizar language is its readability. As is common in mathematical text, it relies on classical logic and a declarative style.[7] Mizar articles are written in ordinary ASCII, but the language was designed to be close enough to the mathematical vernacular that most mathematicians could read and understand Mizar articles without special training.[1] Yet, the language enables the increased level of formality necessary for automated proof checking.
For a proof to be admitted, all steps have to be justified either by elementary logical arguments or by citing previously verified proofs.[8] This results in a higher level of rigor and detail than is customary in mathematical textbooks and publications. Thus, a typical Mizar article is about four times as long as an equivalent paper written in ordinary style.[9]
Formalization is relatively labor-intensive, but not impossibly difficult. Once one is versed in the system, it takes about one week of full-time work to have a textbook page formally verified. This suggests that its benefits are now in the reach of applied fields such as probability theory and economics.[2]
Mizar Proof Checker[edit]
Distributions of the Mizar Proof Checker for all major operating systems are freely available for download at the Mizar Project website. Use of the proof checker is free for all non-commercial purposes. It is written in Free Pascal and the source code is available on GitHub.[21]