Teamwork

The work performed on the formalization is a result of a team effort by the researchers and students of the Institute of Mathematics and Institute of Computer Science, University of Biaystok. MIZAR articles written in the project have been authored by:

Czesaw Byliski, Adam Grabowski, Ewa Grdzka, Jarosaw Gryko, Artur Korniowicz, Beata Madras, Agnieszka J. Marasik, Robert Milewski, Adam Naumowicz, Piotr Rudnicki (University of Alberta, Canada), Bartomiej M. Skorulski, Andrzej Trybulec, Mariusz ynel, and Grzegorz Bancerek.

In the summer of 1995, we started a seminar devoted to the theory of continuous lattices following [7] and [10]. In the spring of 1996, the final decision on formalization of [7] was made. Parts of the first two chapters, O. A Primer of Continuous Lattices and I. Lattice Theory of Continuous Lattices, were assigned to individual team members for formalization. We adopted the following rules:

• formalization is divided into two series of MIZAR articles with the identifiers⁴:
  • YELLOW - articles bridging the MML and the knowledge assumed in the compendium,
  • WAYBEL⁵ - articles formalizing the main course of the compendium,
• no formalization of examples unless necessary,
• the formalization is as close to [7] as possible but taking into account some MIZAR peculiarities such as built-in concepts and mechanisms, possibility of automatic generalization, reuse of the MML, etc.
• the formalization should be more general than the theory in the compendium, e.g. we follow hints at generalization included in exercises (see 1.26 on page 52 of [7] and compare pages 38-42 with [4]).

Because of the number of people involved, the work was organized in a different way than the usual sequential contributions of articles to MML. Usually, an author writes an article and the article is not available to other authors until it is submitted to the MML. We wanted to formalize different parts of the book simultaneously as sequential development would be too slow. We decided to maintain a local library of YELLOW and WAYBEL series with completed and non-completed articles. This allowed for some parallelism in writing articles. The articles from local library were tested by later ones that used them and if there was a need they were revised. After some time they were presented on a seminar to discus possible generalization and, finally, submitted to the MML.

The size of the YELLOW series (17 articles of 49) indicates that MML was almost ready for the formalization. However, the following topics had to be developed:

• upper and lower bounds, suprema and infima (YELLOW_0),
• poset under inclusion (YELLOW_1),
• lattice of ideals (YELLOW_2),
• complete lattices (YELLOW_0 and YELLOW_2),
• Cartesian product of posets and lattices (YELLOW_1, YELLOW_3, and YELLOW10),
• lattice operations on subsets of a poset (YELLOW_4),
• Boolean lattices (YELLOW_2 and YELLOW_5),
• duality in lattices (YELLOW_7),
• modular and distributive lattices (YELLOW11),
• Moore-Smith convergence (YELLOW_6),
• Baire spaces and sober spaces (YELLOW_8),
• bases of topologies (YELLOW_9, YELLOW13, and YELLOW15),
• refinements of topologies (YELLOW_9),
• Hausdorff spaces (YELLOW12),
• product of topological spaces (YELLOW14),
• topological and poset retracts (YELLOW16).

The formalization was a stress test for the MIZAR software. It detected some errors and forced adjusting a number of quantitative parameters. The formalization would not be possible without cooperation with system designers and the Library Committee in improvement of software and a number of revisions to the MML.