This paper reports on M
IZAR formalization of the theory of
continuous lattices included in the
A Compendium of
Continuous Lattices, [
7].
M
IZAR formalization means a formalization of theorems, definitions, and
proofs in the M
IZAR language such that it is accepted by the
M
IZAR system. This effort was originally motivated by the question
whether the M
IZAR system is sufficiently developed as to allow
expressing advanced mathematics. The current state of the
formalization, which includes 49 M
IZAR articles written by 14
authors, suggests that the answer is positive.
The work of the team of authors in cooperation with the Library
Committee
1 and system designers resulted
in improvements of the system towards a more convenient technology
for doing mechanically checked mathematics. It revealed, also,
that the substantial element of the convenience is the incorporation
of computer algebra into M
IZAR system.
