Chapter 1

A Summary of Mizar

Mizar is a general term of a project that formalized the use of computers by the Mizar society lead by Prof. Andrzej Trybulec of Warsaw University in Poland. The Mizar project is carried out by describing mathematical demonstrations by the Mizar language. Mizar was created to describe mathematics by using computers and checking them with a Mizar proof checker on a IBM-PC for Mizar library registration. The purpose of this project is to create a system for checking mathematical thesis. In Mizar, text that have descriptions of mathematical demonstrations are called article. When we write new articles, we can refer to articles that have been previously checked and registered in the Mizar library. When that article is registered in the Mizar library, other articles will be able to refer to it.

    The articles are divided into an environ and main sections. In the environ section, we describe the necessary environment setting for that article and in the main section, the demonstrations themselves are described.

    The articles are described by the Mizar language. The Mizar language is based on the description method of general demonstrations; however, in Mizar, there is a specific method for writing. This will be explained later in more detail.

    We will explain the Mizar language, Mizar proof checker, and the Mizar project.