Conclusions

Our general conclusions are that the MIZAR system seems satisfactory for formalizing advanced mathematics and that MML was a satisfactorily rich base for starting the formalization of the CCL-book. Let us now look at the answers to the questions that were posed for the CCL project as stated in Section .

• The expressive power of the MIZAR language is sufficient for formulating the definitions, theorems, and proofs contained in the CCL-book.
• The contents of MML were reused to a substantial degree with some revisions.
• Different concepts introduced in independent articles could be used together quite smoothly.
• The MIZAR software handled the large amounts of material with no problems after adjusting some quantitative parameters.
• Unfortunately, almost no records were kept that would provide reliable data about the human effort required for this project.

Formalization in MIZAR is still not as convenient as doing mathematics traditionally, but the system is being continually improved. Even now, there are some obvious gains from formalizing mathematics in MIZAR: the results are mechanically checked, the stored knowledge can be browsed electronically, and most importantly all the concepts--no matter how small or simple--must be explicitly stated. These factors provided substantial help for MIZAR authors, especially to the new participants in the project. The machine stored information may be mechanically explored, changed, generalized, and edited. Reorganization of machine readable mathematical texts is much easier than reorganization of such texts written informally and such reorganizations were performed frequently in our project.

The work done in this project resulted in numerous improvements of the MIZAR system and revealed a number of issues which are now being investigated further:

• The current organization of the data base as a loose collection of articles is not very convenient and it is headed for serious problems when the data base becomes larger, say by an order of magnitude. It seems that the library should be based on units having monographical nature as the current organization $^{\:\alph{endnotexboole}}$ of MML leads to the fragmentation of related information.
• We need tools for searching MML, which are better than just textual searches used now. In particular, we need tools for static syntax based searching which can distinguish homonyms, identify synonyms, and take into account hidden arguments of constructors, while eliminating the dependence on identifiers.
• The MIZAR verifier, the heart of this proof assistant, should be furnished with some capabilities for automatic algebraic manipulation by employing techniques from computer algebra.
• Since frequent revisions of MML seem inevitable, there is a need for an automated mechanism which will support this process.
• By focusing improvements to the MIZAR language and its implementation toward:
  • the development of a richer syntax for the formulation of theorems, definitions and proofs,
  • strengthening of the inference checker to shorten proofs,
  • increased flexibility in the type system,
  • the addition of attributes with explicit arguments,
  • a more convenient semantics of structure types
  we can derive great benefits for the development of MML-like repositories.

We would like to end with the following question: who will financially support the development of a sizable data base of formal mathematics? At the moment, finishing the CCL-project depends on the answer.