Mizar Mathematical System
Jump to navigation
Jump to search
A Mizar Mathematical System is a mathematical system
- Context:
- It can include a Formal Mathematical Language (for writing mathematical definitions and mathematical proofs).
- It can include a Proof Assistant, which is able to mechanically check proofs written in this language.
- It can include a library of Formalized Mathematics, which can be used in the proof of new theorems.
- See: Declarative Programming, Automath, OMDoc, HOL Light, Coq, Formal Language, Automated Proof Checking, Mathematical Formalization.
References
2017a
- (Wikipedia, 2017) ⇒ https://en.wikipedia.org/wiki/Mizar_system Retrieved:2017-3-2.
- 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. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.
In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.
- 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. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.
2017b
- (Wikipedia, 2017) ⇒ https://en.wikipedia.org/wiki/Mizar_system#Mizar_language Retrieved:2017-3-2.
- 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 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.
- 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.
2015
- (Bancerek et al., 2015) ⇒ Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. (2015). “Mizar: State-of-the-art and Beyond.” In: Conferences on Intelligent Computer Mathematics, pp. 261-279. Springer International Publishing,
- ABSTRACT: Mizar is one of the pioneering systems for mathematics formalization, which still has an active user community. The project has been in constant development since 1973, when Andrzej Trybulec designed the fundamentals of a language capable of rigorously encoding mathematical knowledge in a computerized environment which guarantees its full logical correctness. Since then, the system with its feature-rich language devised to approximate mathematics writing has influenced other formalization projects and has given rise to a number of Mizar modes implemented on top of other systems. However, the information about the system as a whole is not readily available to developers of other systems. Various papers describing Mizar features have been rather incremental and focused only on particular newly implemented Mizar aspects. The objective of the current paper is to give a survey of the most important Mizar features that distinguish it from other popular proof checkers. We also go a step further and describe most important current trends and lines of development that go beyond the state-of-the-art system.