Introduction

The MIZAR language, developed by Andrzej Trybulec from University of Biaystok MIZAR might be considered as an Esperanto for mathematics and there are some similarities between the two languages. Esperanto was developed in Biaystok by Ludwik Zamenhoff and the development of MIZAR is also based 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 are many translations of books into Esperanto and it is possible to learn the language by reading these translations. There is a large collection of MIZAR texts and we know several people who learned MIZAR by reading them., is a language used for the practical formalization of mathematics. The main goal for the original design of MIZAR was to create a formal system close to the mathematical vernacular used in publications with the requirement that the language be simple enough to enable computerized processing, in particular mechanical verification of correctness. The continual development of MIZAR has resulted in a language, software for checking the correctness of texts written in the language, numerous utility programs, a centrally maintained library of mathematics, and an electronic hyper-linked journal, all available on the Internet. Introductory information on MIZAR can be found in [46] and [17] (an interesting personal account is in [58]). For the rest of this paper, we assume that the reader is at least superficially familiar with these basic texts. However, to set the tone for the main body of the paper we start with some general remarks about the MIZAR system.

The MIZAR style of formalization provides some freedom of expression, but the required rigor assures that the result of the formalization has a unique meaning. When formalizing a theory we introduce definitions, lemmas, and theorems hoping that they will be useful for future developments. This is the essential idea behind developing the MIZAR data base.

The MIZAR language is an attempt to approximate mathematical vernacular in a formal language. There are only 102 reserved words forming a tiny subset of English words which are frequently used in regular mathematical papers. The logic of MIZAR is classical and the proofs are written in the Fitch-Jaskowski style (see [29]). Definitions allow for the introduction of constructors for types, terms, adjectives, and atomic formulae. Proofs consist of a sequence of steps, each step justified by facts proved in earlier steps or separate lemmas, theorems, or schemes of theorems. The MIZAR verifier checks whether each inference step is in its opinion obvious unlike other systems which rely on a fixed set of inference or rewriting rules. The notion of an obvious inference has been addressed in the past by M. Davis [22], P. Rudnicki [43], the Kiev project [23], and more recently by H. Friedman [24].

In the earlier stages of the MIZAR project, there were plans to test the MIZAR system by building libraries based on various axiomatics: ZFC for ``normal'' mathematics, Peano axioms for theoretical arithmetic, etc. Because of the substantial effort needed to build such libraries, a decision was made around 1988 to focus on developing one such library--MIZAR Mathematical Library (MML)--based on the Tarski-Grothendieck set theory.

We would like to stress the distinction between MIZAR as a formal system of general applicability (which as such has little in common with any set theory) and the specific application of MIZAR in developing MML which is based entirely on a set theory (see [48]). In building MML, the MIZAR language and set theory provide an environment in which all further mathematics is developed. This development is definitional: new mathematical objects can be defined only after supplying a model for them in the already available theories.

MIZAR provides some elements of second order logic using schemes of theorems. Schemes are expressed with free second order variables and thus may be used to formulate induction schemes, for example.

Multi prefixed structures allow us to introduce algebraic concepts, for example topological groups which are both groups and topological spaces; the account of basic algebraic structures developed in MIZAR is given in [45].

The tools in the MIZAR software collection support some typical tasks of doing mathematics:

• developing and managing mathematical knowledge,
• verifying logical correctness of reasonings,
• beautifying MIZAR texts, e.g., finding irrelevant premises of an inference step or discovering unused text items,
• presenting MIZAR texts using TEX and HTML.

The development of MML has been the main activity of the MIZAR project since the late 1980's as it has been believed within the project team that only substantial experience may help in improving the system. Freek Wiedijk noticed in [59]:

A good system without a library is useless. A good library for a bad system is still very interesting (the system might be improved or the library might be ported to a different, better system). So the library is what counts.

One of the largest concentrated effortsOther areas in which MML has been developed in a focused way are: Jordan's curve theorem, formal treatment of computations and circuits, real and complex analysis, and algebra for symbolic computations. in developing MML has been the formalization of A Compendium of Continuous Lattices [25] in its entirety. This project started in 1996 and we report the state of this endeavor as of April 2002. A smaller report on the project as of March 2000 appeared in [14].

Dana Scott has raised an interesting question of copyright. The CCL-book is copyrighted by Springer-Verlag. Are we violating any copyrights by formalizing the book in MIZAR? It is not clear to us but we hope not and suffice it to say that no part of the book has been copied verbatim.

The plan of this paper is as follows. In Section  we explain the purpose of formalizing the CCL-book at all and the expected results. Section  presents the logistics of the project. The next section presents the MIZAR rendition of basic notions in the CCL-book and background material assumed by the authors of [25] for their readers. We elaborate on parts of this material that required substantial effort to formalize. Section  discusses the issues encountered while formalizing the main body of the CCL-book. The next two sections offer some data about the length of the formal texts and estimates of the human effort of this project. Section  draws conclusions while also presenting our plans for the future.