Organizers:

• Jesse Alama, Center for Artificial Intelligence, New University of Lisbon, Portugal
• Adam Grabowski, Institute of Mathematics, University of Bialystok, Poland
• Artur Kornilowicz, Institute of Informatics, University of Bialystok, Poland
• Adam Naumowicz, Institute of Informatics, University of Bialystok, Poland
• Piotr Rudnicki, Department of Computing Science, University of Alberta, Canada
• Josef Urban, Computing Science Department, Radboud University, The Netherlands

Brief description of the tutorial's goals and topics to be covered:

The tutorial will provide an overview of how the Mizar system can be used for practical computer formalization of mathematical theorems. The system is best noted for its formal language derived from informal mathematics and the world's largest repository of formalized and computer-checked mathematical knowledge, the Mizar Mathematical Library (MML).

The main goal of the tutorial is to help the attendees get acquainted with basic Mizar terminology by exploring the expressiveness of the Mizar language and the capabilities of the verification system. After attending the tutorial, the participants should be ready to understand all Mizar texts available in MML and start individual experiments with writing and verifying their own proofs using Mizar.

By design, Mizar supports writing proofs in a declarative way resembling the standard mathematical practice. The proofs written in Mizar are constructed according to the rules of the Fitch-Jaskowski style of natural deduction. The Mizar way of writing proofs was also the model for the notion of 'formal proof sketches' developed by F. Wiedijk. Presenting the essential methods of constructing proofs with appropriate examples will be a part of the tutorial. Also some ways of automating reasonings with so called registrations, properties and identifications will be demonstrated.

All Mizar developments have been created in a steady fashion on top of the chosen axiomatics and previously formalized data. MML is today a collection of interrelated texts (articles) fully checked for correctness by the Mizar checker, based on the axioms of the Tarski-Grothendieck set theory. The most recent distribution of the MML (version 4.160.1126) includes 1122 articles comprising 51244 theorems and 9993 definitions (using 7281 different symbols) written by 236 authors from Canada, China, Czech Republic, Germany, Italy, Japan, the Netherlands, Poland, Russia and USA. To help the new users start working with the huge library, the basic structure of a Mizar article as well as the MML's organization, current development and methods of maintenance will be showed.

To facilitate the whole process of writing formal mathematics, several utility programs and external systems have been developed that complement the Mizar proof checker, e.g. improving the author's formalizations or enabling effective semantic-based information retrieval and presentation of the MML contents and providing proof advice with external ATP and AI tools. It is now also possible to collaboratively use the Mizar processor to develop formalizations in an on-line Wiki-based environment. The use and capabilities of these tools will be demonstrated.

• Introduction
• Proof example
• On-line mini-tutorial