Main directions in the development of the Mizar Mathematical Library

• Formalization of Jordan Curve Theorem
• Formalization of 'A Compendium of Continuous Lattices'
• The theory of random access Turing machines