Mizar system
Proof assistant program
- 4 min read
- 4 chapters
Related on Lably
Through ASCII, Economics and Natural number
In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.
History
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. 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.
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, the Mizar Mathematical Library—the sizable body of formalized mathematics that it verified—is licensed open-source.
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.
Sign in to keep reading
3 more chapters are free with a Lably account.
Mizar language
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. 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. 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. 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.
Formalization can be labor-intensive and difficult. Formally verifying a single textbook page can take a week of full-time work. The benefits may be within reach in applied fields such as probability theory and economics.
Mizar Mathematical Library
The Mizar Mathematical Library (MML) includes all theorems to which authors can refer in newly written articles. Once approved by the proof checker they are further evaluated in a process of peer-review for appropriate contribution and style. If accepted they are published in the associated Journal of Formalized Mathematics and added to the MML.
Breadth
As of July 2012, the MML included 1150 articles written by 241 authors. In aggregate, these contain more than 10,000 formal definitions of mathematical objects and about 52,000 theorems proved on these objects. More than 180 named mathematical facts have been given formal codification in this manner. Some examples are the Hahn–Banach theorem, Kőnig's lemma, the Brouwer fixed point theorem, Gödel's completeness theorem, and the Jordan curve theorem.
This breadth of coverage has led some to suggest Mizar as one of the leading approximations to the QED utopia of encoding all core mathematics in computer verifiable form.
Availability
All MML articles are available in PDF form as the papers of the Journal of Formalized Mathematics. The full text of the MML is distributed with the Mizar checker and can be freely downloaded from the Mizar website. In an ongoing recent project the library was also made available in an experimental wiki form that only admits edits when they are approved by the Mizar checker.
The MML Query website implements a search engine for the contents of the MML. Among other abilities, it can retrieve MML theorems proved about a particular type or operator.
Logical structure
The MML is built on the axioms of the Tarski–Grothendieck set theory. Even though semantically all objects are sets, the language allows one to define and use syntactical weak types. For example, a set may be declared to be of type Nat only when its internal structure conforms with a particular list of requirements. In turn, this list serves as the definition of the natural numbers and the set of all the sets that conform to this list is denoted as NAT. This implementation of types seeks to reflect the way most mathematicians formally think of symbols and so streamline codification.
Mizar Proof Checker
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.