An example of formalizing recent mathematical results in Mizar

This paper describes an example of the successful formalization of quite advanced and new mathematics using the Mizar system. It shows that although much effort is required to formalize nontrivial facts in a formal computer deduction system, still it is possible to obtain the level of full logical correctness of all inference steps. We also discuss some problems encountered during the formalization, and try to point out some of the features of the Mizar system responsible for that. The formalization described in this paper allows also for contrasting the linguistic capability of the Mizar language and some of the phrases commonly used in “informal” mathematical papers that the Mizar system lacks, and consequently presents the methods of how to cope with it during the formalization. Yet, apart from the problems, this paper shows some definite benefits from using a formal computer system in the work of a mathematician.