To formalize means to investigate some mathematical theory rigorously, obeying fixed rules of formulating, defining, proving, and reasoning. MIZAR formalization admits some variety of expression but the required rigor assures that the result of the formalization, that is a text in the context of the MIZAR system, has unique meaning. When formalizing a theory we introduce definitions, lemmas, and theorems with the hope that they will be useful for future developments. This is the essential idea behind developing the MIZAR data base.
MIZAR2 has been designed by Andrzej Trybulec and developed by a team under his leadership. The system includes a language, software tools, a library, and a hyperlinked journal.
The MIZAR language is an attempt to approximate mathematical
vernacular in a formal language. Reserved words form a subset of
English words which are used in regular mathematical papers with the
same meaning. The logic of MIZAR is classical, the proofs are
written in the Fitch-Ja
kowski style, see [9].
Definitions allow to introduce type, term, and formula constructors
and require proving of correctness conditions. A proof consists of a
sequence of steps, each step justified by facts proved in earlier
steps, lemmas, theorems and/or schemes. Schemes are second order
theorems which may be used to formulate e.g. induction. Multi prefixed
structures allow to introduce algebraic concepts, for example topological
groups which are both groups and topological spaces. More detailed
description of MIZAR system can be found in [6],
[18], and, also, in [13].
MIZAR software includes tools supporting some typical tasks when doing mathematics:
The Mizar Mathematical Library (MML) is a collection of texts written in MIZAR language called Mizar articles. The MML is based on the Tarski-Grothendieck set theory. As of March 2000 there were 633 articles collected. They included 29,514 theorems, 5,389 definitions and redefinitions, and 317,427 references to external theorems (i.e. in other articles).
Mizar articles are automatically translated into English and published in Formalized Mathematics. The electronic version, Journal of Formalized Mathematics, http://www.mizar.org/JFM/ includes hyper-links to definitions which substantially help in using the MML. More details may be found on MIZAR web pages at http://www.mizar.org/.
MIZAR might be considered as an Esperanto for mathematics and there
are some similarities between both languages. Esperanto was developed
in Bia
ystok by L. Zamenhoff and MIZAR is being developed in
Biaystok. Esperanto is an artificial international language with
words taken from several national languages and uses a quite regular grammar.
MIZAR may be considered as an attempt to standardize the
language of mathematics. There is a lot of translations of
books into Esperanto and it is possible to learn the language by
reading those translations. There is a large collection of MIZAR articles and it is possible to learn MIZAR (and mathematics) by
reading them.