An Overview of the MIZAR Project

The Mizar project is a long-term effort aimed at developing software to support a working mathematician in preparing papers. A. Trybulec, the leader of the project, has designed a language for writing formal mathematics. The logical structure of the language is based on a natural deduction system developed by Ja'skowski. The texts written in the language are called Mizar articles and are organized into a data base. The Tarski-Grothendieck set theory forms the basis of doing mathematics in Mizar. The implemented processor of the language checks the articles for logical consistency and correctness of references to other articles