A Compendium of Continuous Lattices in MIZAR

Abstract. This paper reports on the Mizar formalization of the theory of continuous lattices as presented in A Compendium of Continuous Lattices, [25]. By the Mizar formalization we mean a formulation of theorems, definitions, and proofs written in the Mizar language whose correctness is verified by the Mizar processor. This effort was originally motivated by the question of whether or not the Mizar system was sufficiently developed for the task of expressing advanced mathematics. The current state of the formalization--57 Mizar articles written by 16 authors-indicates that in principle the Mizar system has successfully met the challenge. To our knowledge it is the most sizable effort aimed at mechanically checking some substantial and relatively recent field of advanced mathematics. However, it does not mean that doing mathematics in Mizar is as simple as doing mathematics traditionally (if doing mathematics is simple at all). The work of formalizing the material of [25] has: (i) prom...

• Type: Journal
• Year: 2002
• Where: JAR
• Authors: Grzegorz Bancerek, Piotr Rudnicki
• Keywords: Continuous Lattices, JAR 2002, Mizar Formalization, Mizar System