The Mizar system consists of a
formal language
In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.
The alphabet of a formal language consists of symb ...
for writing mathematical definitions and proofs, a
proof assistant
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
, 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
Andrzej Wojciech Trybulec (29 January 1941 in Kraków, Poland – 11 September 2013 in Białystok, Poland) was a Polish mathematician and computer scientist noted for work on the Mizar system.
Early years
His parents Jan W. Trybulec and Barbara ...
.
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
Andrzej Wojciech Trybulec (29 January 1941 in Kraków, Poland – 11 September 2013 in Białystok, Poland) was a Polish mathematician and computer scientist noted for work on the Mizar system.
Early years
His parents Jan W. Trybulec and Barbara ...
as an attempt to reconstruct mathematical
vernacular
A vernacular or vernacular language is in contrast with a "standard language". It refers to the language or dialect that is spoken by people that are inhabiting a particular country or region. The vernacular is typically the native language, n ...
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
The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. ( Q.E.D. means in Latin, meaning "which was to be demonstrated.")
Overview
T ...
.
Currently the project is developed and maintained by research groups at
Białystok University
Białystok is the largest city in northeastern Poland and the capital of the Podlaskie Voivodeship. It is the tenth-largest city in Poland, second in terms of population density, and thirteenth in area.
Białystok is located in the Białystok Up ...
, Poland, the
University of Alberta
The University of Alberta, also known as U of A or UAlberta, is a public research university located in Edmonton, Alberta, Canada. It was founded in 1908 by Alexander Cameron Rutherford,"A Gentleman of Strathcona – Alexander Cameron Rutherfor ...
, Canada, and
Shinshu University
, abbreviated to , is a Japanese national university located in Matsumoto, Nagano Prefecture, Japan. As the only university in Japan bearing the name of a former Japanese province, it bears the name "Shinshu" (alternative name for Shinano Pr ...
, Japan. While the Mizar proof checker remains proprietary,
[Mailing list discussion](_blank)
referring to the close-sourcing of Mizar. the Mizar Mathematical Library—the sizable body of formalized mathematics that it verified—is licensed open-source.
referring to the open-sourcing of MML.
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
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
'', ''
Journal of Automated Reasoning
The ''Journal of Automated Reasoning'' was established in 1983 by Larry Wos, who was its editor in chief until 1992. It covers research and advances in automated reasoning, mechanical verification of theorems, and other deductions in classical and ...
'' and the ''
Journal of Formalized Reasoning
The ''Journal of Formalized Reasoning'' is a peer-reviewed open access academic journal established in 2009. It publishes mathematical formalization, formalization efforts in any area, including classical mathematics, constructive mathematics, form ...
''.
Mizar language
The distinctive feature of the Mizar language is its readability. As is common in mathematical text, it relies on
classical logic
Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this class ...
and a
declarative style. Mizar articles are written in ordinary
ASCII
ASCII ( ), abbreviated from American Standard Code for Information Interchange, is a character encoding standard for electronic communication. ASCII codes represent text in computers, telecommunications equipment, and other devices. Because of ...
, 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
Probability theory is the branch of mathematics concerned with probability. Although there are several different probability interpretations, probability theory treats the concept in a rigorous mathematical manner by expressing it through a set o ...
and
economics
Economics () is the social science that studies the Production (economics), production, distribution (economics), distribution, and Consumption (economics), consumption of goods and services.
Economics focuses on the behaviour and intera ...
.
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
Peer review is the evaluation of work by one or more people with similar competencies as the producers of the work (peers). It functions as a form of self-regulation by qualified members of a profession within the relevant field. Peer review ...
for appropriate contribution and style. If accepted they are published in the associated ''Journal of Formalized Mathematics''
[''Journal of Formalized Mathematics''](_blank)
/ref> and added to the MML.
Breadth
As of July 2012, the MML included 1150 articles written by 241 authors.[The MML Query search engine](_blank)
/ref> 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 so benefited from formal codification. Some examples are the Hahn–Banach theorem
The Hahn–Banach theorem is a central tool in functional analysis.
It allows the extension of bounded linear functionals defined on a subspace of some vector space to the whole space, and it also shows that there are "enough" continuous linear f ...
, Kőnig's lemma
Kőnig's lemma or Kőnig's infinity lemma is a theorem in graph theory due to the Hungarian mathematician Dénes Kőnig who published it in 1927. It gives a sufficient condition for an infinite graph to have an infinitely long path. The computab ...
, Brouwer fixed point theorem
Brouwer's fixed-point theorem is a fixed-point theorem in topology, named after L. E. J. (Bertus) Brouwer. It states that for any continuous function f mapping a compact convex set to itself there is a point x_0 such that f(x_0)=x_0. The simplest ...
, Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.
The completeness theorem applies to any first-order theory: I ...
and Jordan curve theorem
In topology, the Jordan curve theorem asserts that every ''Jordan curve'' (a plane simple closed curve) divides the plane into an " interior" region bounded by the curve and an "exterior" region containing all of the nearby and far away exterior ...
.
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
Portable Document Format (PDF), standardized as ISO 32000, is a file format developed by Adobe in 1992 to present documents, including text formatting and images, in a manner independent of application software, hardware, and operating systems. ...
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
A wiki ( ) is an online hypertext publication collaboratively edited and managed by its own audience, using a web browser. A typical wiki contains multiple pages for the subjects or scope of the project, and could be either open to the pu ...
form[The MML in wiki form](_blank)
/ref> that only admits edits when they are approved by the Mizar checker.
The MML Query website implements a powerful search engine for the contents of the MML. Among other abilities, it can retrieve all MML theorems proved about any particular type or operator.
Logical structure
The MML is built on the axioms of the Tarski–Grothendieck set theory
Tarski–Grothendieck set theory (TG, named after mathematicians Alfred Tarski and Alexander Grothendieck) is an axiomatic set theory. It is a non-conservative extension of Zermelo–Fraenkel set theory (ZFC) and is distinguished from other axiom ...
. 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
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal n ...
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
Free Pascal Compiler (FPC) is a compiler for the closely related programming-language dialects Pascal and Object Pascal. It is free software released under the GNU General Public License, witexception clausesthat allow static linking against it ...
and the source code is available to all members of the Association of Mizar Users.[The Association of Mizar Users website](_blank)
/ref>
See also
* Isar (Isabelle)
The Isabelle automated theorem prover is a HOL (proof assistant), higher-order logic (HOL) theorem prover, written in Standard ML and Scala (programming language), Scala. As an LCF theorem prover, LCF-style theorem prover, it is based on a small ...
* Metamath
Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in ...
References
External links
*
{{authority control
Large-scale mathematical formalization projects
Proof assistants
Dependently typed languages
Educational math software
Mathematical societies
Pascal (programming language) software
Programming languages created in 1973