ICM 1998, Berlin, Aug. 18–27

Abstracts of Short Communications and Posters

Section:

1. Logic

1991 MS Classification: 6, 3 Bancerek, Grzegorz, A., University of Białystok, Poland Mizar - a work environment for a mathematician: an experiment with continuous lattices The Mizar system is centered around a language for recording mathematics in a traditional style and a collection of Mizar articles (over 500), mechanically checked for correctness, published in Journal of Formalized Mathematics – http://mizar.org/JFM/ . Mizar articles develop mathematics starting with the Tarski-Grothendieck set theory. As an experiment testing the practicability of the Mizar system for doing mathematics we have decided to formalize the theory of continuous lattices as presented in “A Compendium of Continuous Lattices”. The Mizar text is no more than 10 times longer than the text in the book. The experiment shows that we can formalize and check some advanced theories.