Goal and Motivations

At the QED³Workshop II, Warsaw 1995, the following question was raised:

Can we do formalization of advanced mathematics like this included in regular mathematical books in the current proof-checking systems?

In trying to answer this question we have decided to put MIZAR into a serious test. We have chosen A Compendium of Continuous Lattices [7] to be formalized in its entirety. The theory of continuous lattices presented in [7] is mathematically advanced. It involves a variety of areas of mathematics: computation, topology, analysis, algebra, category theory, and logic. Also, it is a relatively recent and a well-established field. The choice turned out to be a lucky one. The compendium is very rigorous which made the formalization comparatively easy; also, some initial fragments of the theory of lattices had been already developed in MIZAR.

In the past, there were some attempts to formalize entire mathematical books in computerized proof-checking systems. In the 1970's, Jutting [17] formalized Landau's Grundlagen [12] in AUTOMATH. Another attempt was the formalization of 2 chapters of Theoretical Arithmetic by Grzegorczyk, [8], in the 1980's. It was done by A. Trybulec's team in MIZAR 2, which was not equipped with the library. In MIZAR 2, each text was processed separately from other texts. All background knowledge needed to write a text was put without proofs in a preliminary section.

In 1989 we started to collect all MIZAR texts and on this basis develop and maintain the Mizar Mathematical Library. Each new MIZAR article can be submitted to the MML if it is accepted by the MIZAR verifier and refers only to articles already included in the MML. At the start, the basis of the MML was formed by two axiomatic articles:

• Tarski Grothendieck set theory [15],
• Built-in concepts [14], including strong arithmetic of real numbers.

The latter became a regular MIZAR article in 1998 when the construction of real numbers was completed.

The experiment with formalization of an entire book has many aspects and we expected to get answers to the following:

• Is the MIZAR language sufficiently expressive to formulate definitions, theorems, and proofs contained in [7]?
• Is MML rich enough to even start the formalization? Did MML cover the knowledge assumed in the compendium as background?
• Can the different concepts already defined in independent articles in MML be used together?
• Is the MIZAR software capable of handling this amount of material?

We hoped that running such an experiment, irrespective of the answers to the above questions, would lead to an improvement of MIZAR.