Our main conclusion is that the Mizar system seems satisfactory for formalizing advanced mathematics. But, formalization in Mizar is still not as simple as doing mathematics traditionally. It is the result of having to meet the requirements of a more restrictive automatic reviewer than the traditional human one. We must also mention that careful anticipation of future reuse of information is needed to realize such projects. On the other hand, since the Mizar text is machine readable, it would be natural to expect the development of a powerful computer aid for writing Mizar articles. This requirement seems to be the most important to make Mizar a system devoted to a wider team of users, not only for highly qualified Mizar experts.
Acknowledgments: We would like to thank to all active and past members of the project for their engagement and fruitful work. The list of members of the project, excluding the first and the second authors of this paper, is as follows