Tutorial: Exploring the Mizar Mathematical Library (EMML 2019)

(organizers/presenters: Adam Naumowicz, Artur Kornilowicz, Adam Grabowski)

The participants of this tutorial will be able to get familiar with the structure and organization of the Mizar library and learn about various ways of exploring it. It should be of interest to new users, those who want to become more proficient in formalizing with Mizar, as well as those who are interested in sharing and exchanging mathematical data across different formalisms.

The main focus points will be on:

• methods of interacting with the library from the user's perspective,
• tools and resources used by the developers,
• data formats used for storing formalized information and presenting its contents,
• routine tasks and challenges of maintaining the repository,
• main areas of mathematics covered in the current library.

The proposed tutorial is a follow-up to the Mizar hands-on tutorial which was conducted at CICM 2016 in Bialystok. However, the knowledge of the Mizar language will not be prerequisite.