Goals and Motivation

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

The above question was raised at the 2nd QED Workshop held in Warsaw in 1995. In trying to answer this question we followed Ralph Wachter's suggestion to put MIZAR under a stress test by starting the formalization of A Compendium of Continuous Lattices [25] in its entirety. The project officially started in April 1996. The theory of continuous lattices presented in [25] is a relatively recent and a well-established field; it is mathematically advanced and involves a variety of areas: algebra, general topology, analysis, category theory, logic, topological algebra, and also touches on the theory of computation. The choice turned out to be a lucky one. Foremost, the compendium is very rigorous which made the formalization comparatively easy (this is a hindsight view). Also, some initial fragments of the theory of lattices had been already developed in MIZAR (see Section ).

In the past, there were some attempts to formalize entire mathematical books in computerized proof-checking systems. The best known example was done in the 1970's when L. S. Jutting formalized Landau's Grundlagen der Analysis in de Bruijn's AUTOMATH system (see  [31,35,40]). We are sure that in other proof assistants, people have been undertaking similar efforts of formalizing mathematical books, but we are aware of only two partially completed attempts: D. L. Simon in his 1990 PhD thesis at University of Texas at Austin checked The elementary theory of numbers by Leveque using the Boyer-Moore prover, and in the 1980's, J. Siekmann's group from Saarbrücken started checking Düssen's Halbgruppen und Automaten with the help of the MKRP prover.

Also in the 1980's, there was an attempt to formalize two chapters of Theoretical Arithmetic by Grzegorczyk [28] in an earlier version of MIZAR called MIZAR-2 by a team led by A. Trybulec. In MIZAR-2, each text was self contained as there was no library. As a consequence, all background knowledge needed to verify a text was put into a preliminary section which was checked only for syntactic correctness.

Since 1989, the focus of the MIZAR project has been the development of a knowledge base called MIZAR Mathematical Library (MML), a collection of texts written in the MIZAR language called MIZAR articles. New MIZAR articles can be submitted to MML if they are accepted by the MIZAR verifier and refer only to articles that already have been included in MML. The starting point of MML consisted of two axiomatic articles:

• Tarski Grothendieck set theory in TARSKI [48], containing the axioms of Zermelo-Fraenkel set theory with the axiom of infinity replaced by Tarski's axiom on the existence of arbitrarily strong inaccessible cardinals (axiom of choice is then proven as a theorem);
• Built-in concepts in AXIOMS [49], containing axiomatics of strong arithmetic of real numbers.

The latter article became a regular MIZAR article in 1998 when the construction of real numbers was completed (in the ARYTM series of articles [10,54,55,37]). Thus the fundamental properties of real numbers became proven theorems rather than axioms, but the article is still named AXIOMS causing some confusion for newcomers.

Table  gives some quantitative data about MML at the start of the CCL project and at the time of this writing. In this table, an external reference is a reference from a MIZAR article to another article in MML.

Table I: MML: now and then

	Articles	Size	Theorems	Definitions	External
		in kbytes			references
April '96	425	25,118	22,863	4,193	163,999
April '02	717	52,185	31,741	6,093	371,795

Any experiment with formalization of an entire book has many aspects and before starting CCL we expected to get answers or at least some insight into the following:

• Is the MIZAR language sufficiently expressive to formulate definitions, theorems, and proofs contained in the CCL-book?
• Is MML rich enough to even start the formalization? To what degree does MML cover the knowledge assumed in the CCL-book as background?
• To what degree can different concepts already defined in independent articles in MML be used together?
• Is the MIZAR software capable of handling this amount of material?
• What is the human effort required for such a formalization?

We hoped that running such an experiment, irrespective of the answers to the above questions, would lead to an improvement of MIZAR since all of the development team members were also involved in the CCL project and would work on the necessary changes. The current development team includes: G. Bancerek, Cz. Bylinski, A. Korniowicz, A. Naumowicz, and A. Trybulec.