Mizar system
| Mizar | |
|---|---|
| Paradigms : | declarative |
| Publishing year: | 1973 |
| Designer: | Andrzej Trybulec |
| Developer: | Andrzej Trybulec |
| Typing : | static , weak |
| Influenced by: | Automath |
| Affected: | OMDoc , HOL Light , Coq |
| http://www.mizar.org/ | |
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant that mechanically checks evidence captured in this language , and a library of formalized mathematics that can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project , formerly under the direction of its founder Andrzej Trybulec .
The Mizar Mathematical Library is the world's largest collection of strictly formalized mathematics.
history
The Mizar project was started in 1973 by Andrzej Trybulec in an attempt to reconstruct the mathematical terminology in such a way that it can be checked by a computer. The current goal, in addition to further development of the Mizar system, is the collaborative creation of a large library of formally verified evidence, which should cover the majority of modern mathematics. This is entirely in line with the QED manifesto .
The project is currently being maintained and developed by research groups from the University of Białystok (Poland), the University of Alberta (Canada) and Shinshū University (Japan). While the evidence verification program remains proprietary , the Mizar Mathematical Library - the library of formally verified mathematics - is open-source licensed.
Papers related to the Mizar system appear regularly in journals of the Academic Society for Mathematical Formalization. These include Studies in Logic, Grammar and Rhetoric , Intelligent Computer Mathematics , Interactive Theorem Proving , Journal of Automated Reasoning, and the Journal of Formalized Reasoning .
Surname
According to Andrzej Trybulec, the double star Mizar in the constellation of the Big Dipper is the namesake of the project.
Mizar language
The outstanding feature of the Mizar language is its readability. As usual with mathematical texts, it is based on classic logic and declarative style . Mizar articles are written in ordinary ASCII , but the language was designed to be close enough to mathematical terminology that most mathematicians can understand Mizar articles without special training. Nevertheless, the language allows for an increased degree of formality, necessary for automatic evidence checking.
In order for a proof to be accepted, all steps must be justified, either with elementary logical arguments or by quoting already verified evidence. This results in a higher level of detail than usual in normal mathematical textbooks and publications. Because of this, a typical Mizar article is about four times longer than an equivalent paper written in a common style.
Formalizing a theorem in the Mizar language is relatively laborious, but not impossibly difficult. Once you are familiar with the system, it takes about a week of full-time work to have a textbook page formally verified. This suggests that the benefits of the system are within reach of applied areas such as probability theory and economics .
Mizar Mathematical Library
The Mizar Mathematical Library (MML) contains all the theorems to which new articles may refer. Once articles are accepted by the Evidence Reviewer, they are further externally peer reviewed and the style and value of the submission examined. If they are accepted, they will be published in the own Journal of Formalized Mathematics and added to the MML.
width
In July 2012, the MML comprised 1,150 articles written by 241 authors. Together, these comprise more than 10,000 formal definitions of mathematical objects and approximately 52,000 proven theorems about these objects. More than 180 named mathematical facts could be formally coded. Examples are Hahn-Banach's theorem , König's lemma , Brouwer's fixed point theorem , Gödel's completeness theorem and the Jordanian curve theorem .
The breadth of coverage led some people to suggest Mizar as one of the leading approximations to the QED Manifesto , the coding of all mathematics in computer verifiable form.
Availability
All MML articles are available in PDF form as papers in the Journal of Formalized Mathematics . All text in the MML is distributed using the Mizar Proof Checker and can be downloaded for free from the Mizar website. In an ongoing project, the library was made available in an experimental wiki format that only allows edits if they are accepted by the proof checker.
The Query website implements a powerful search engine for the content of the MML. Among other things, it can list all MML theorems that have been proven about a particular type or operator.
Logical structure
The MML is based on the axioms of the Tarski-Grothendieck set theory . Although semantically all objects are sets , the language allows the definition and use of weak types . For example, a set can only be declared as type Nat if its internal structure conforms to a certain list of requirements. In return, this list serves as a definition of the natural numbers and the set of all sets that conform to this list is called NAT . This implementation of types seeks to mirror the way most mathematicians think of symbols, making the process of coding easier.
Mizar Proof Checker
Distributions of the Mizar Proof Checker for the common operating systems are freely available for download from the Mizar website. The use of the Proof Checker is free of charge for non-commercial applications. The software was written in Free Pascal and the source code is available to all members of the Association of Mizar Users.
See also
Web links
- Official website
- Writing a Mizar article in nine easy steps (PDF; 285 kB), an introduction to the Mizar language
- Mizar in a Nutshell
Individual evidence
- ↑ a b Adam Naumowicz, Artur Korniłowicz: A Brief Overview of Mizar . In: Theorem Proving in Higher Order Logics . 5674, 2009, pp. 67-72.
- ^ A b Freek Wiedijk: Formalizing Arrow's theorem . In: Sadhana . 34, No. 1, 2009, pp. 193-220.
- ^ Roman Matuszewski, Piotr Rudnicki: Mizar: the first 30 years . In: Mechanized Mathematics and Its Applications . 4, 2005.
- ^ Freek Wiedijk: Mizar . Retrieved July 2012.
- ↑ Mailing list discussion ( Memento of the original from October 9, 2011 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice. referring to the close-sourcing of Mizar.
- ↑ Mailing list announcement referring to the open-sourcing of MML.
- ^ Mizar The first 30 Years ( Memento from September 27, 2006 in the Internet Archive )
- ↑ H. Geuvers: Proof assistants: History, ideas and future . In: Sadhana . 34, No. 1, 2009.
- ^ Freek Wiedijk: Formal Proof - Getting Started . In: AMS Special Issue on Formal Proof . 2008.
- ↑ a b Journal of Formalized Mathematics
- ↑ a b The MML Query search engine
- ^ A list of named theorems in the MML . Retrieved July 2012.
- ^ Freek Wiedijk: The QED Manifesto Revisited . In: From Insight to Proof: Festschrift in Honor of Andrzej Trybulec . 10, No. 23, 2007.
- ↑ Page no longer available , search in web archives: The MathWiki project homepage
- ↑ The MML in wiki form ( Memento of the original dated December 2, 2013 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice.
- ^ Jesse Alama, Kasper Brink, Lionel Mamane and Josef Urban: Large Formal Wikis: Issues and Solutions . In: Intelligent Computer Mathematics . 6824, 2011, pp. 133-148.
- ↑ An example of an MML query , yielding all theorems proved on the exponent operator, by the number of times they are cited in subsequent theorems.
- ^ Another example of an MML query , yielding all theorems proved on sigma fields .
- ↑ Adam Grabowski, Artur Kornilowicz, Adam Naumowicz: Mizar in a Nutshell . In: Journal of Formalized Reasoning . 3, No. 2, 2010, pp. 152–245.
- ^ Paul Taylor: Practical Foundations of Mathematics . Cambridge University Press, 1999, ISBN 9780521631075 .
- ^ The Association of Mizar Users website
