Conclusions

Our main conclusion is that the MIZAR system seems satisfactory to formalize advanced mathematics.

The second conclusion is that the MML was satisfactorily rich to start formalization of the compendium. The YELLOW series constitutes only 35% of the whole project.

Formalization in MIZAR is still not as simple as doing mathematics traditionally. It should be improved in near future. Now, however, there are some gains. The results are mechanically checked. There is an automatic access to the knowledge stored and the net of concepts is explicit. (This helped very much for new authors to start.) The information may be mechanically explored: changed, generalized, and edited. Reorganization of a machine readable mathematical text is much easier than reorganization of such a text written on paper. (Such reorganizations were quite often required in our project.)

The work done in this project resulted in numerous improvements of the MIZAR system and, also, it revealed a number of issues that are investigated:

• tools for searching MML: semantic searching which can distinguish homonyms, glue synonyms, and recognize hidden arguments,
• proof assistance based on the exploration of existing proofs in the MML and computer algebra,
• reorganization of the MML: revisions of existing articles and "online revision" mechanism available by environment directives,
• development of MIZAR language to improve the convenience of formulation of definitions and proofs, the length of proofs, and the flexibility of type structure: type modifier, attributes with explicit arguments, new realization of structure types.