Although the Mizar formalization of the theory of continuous lattices already includes 57 articles, there is still a lot of work to do. The continuation of the formalization presented in this paper should result in the proof of equivalence of Lawson topology and lim-inf topology. This will cover Chapter III of [CCL].
The most difficult topic on the project research frontier seems to be the theory of function spaces (Chapter II of [CCL]). It deals with categorial properties unifying the lattice aspects of function spaces with topological ones. Namely, we must address lattice and topological products, top-lattices of maps preserving some lattice properties and top-lattices of continuous topological maps, and correspondence between them in this topic. It is well advanced (see [W27]), but still some theorems are waiting.
Chapters 0 and I are already covered. Also, the formalization of Chapters IV and V is started. However, the theory from Chapter V needs equivalence of Lawson and lim-inf topologies and formalized results cannot be submitted yet to the MML. For Chapter IV there were and still are several formalizations needed to fill the gaps between knowledge assumed in the book [CCL] and the state of the MML. For example, the latest gap filled concerns concrete categories which are used to develop the duality theory from Chapter IV. The duality is based on Galois connection and concerns lattices and maps investigated in previous chapters.