Mizar (software)

Mizar is a mathematical software system that includes a language for writing formalized definitions and proofs, and a high-level program that interprets the language and either accepts or rejects proofs, together with a library of definitions and already proved theorems which can be referenced and used in new proofs.

The Mizar software is available for free ; distributions for various operating systems can be downloaded.

History

The development of Mizar was started in 1973 as an attempt to emulate the natural language of mathematics from its very beginning, starting with the most basic mathematical objects. It was created by Andrzej Trybulec and is now maintained at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan.

The language and its interpretation

Mizar programs are written as plain ASCII files. The standard extension "miz" is recommended (but not required); thus a program usually is named as something.miz.

This program can be interpreted with command "mizf", for example,

mizf something

or

mizf something.miz

A misar program is assumed to consist of lines. The interpreter checks the program line by line and, for each line, either accepts or rejects it. Accepted lines are considered to be proven. Lines of the input file that are not accepted are marked by the software. If all the lines are accepted, then all the theorems formulated in the program are considered as proven. If the mizar program is not accepted as a whole, the lines marked as rejected have to be corrected and/or supplied with an additional proof.

Mizar libraries

The Mizar distribution includes the Mizar Mathematical Library (MML) consisting of definitions and theorems which can be referred to in newly written articles. These new articles, after having been reviewed and checked automatically, can be published in the associated Journal of Formalized Mathematics

For the beginning of year 2010, the Mizar Mathematical Library (version 4.130.1076) includes 1073 articles written by 226 authors and 49548 theorems, 9487 definitions, 785 schemes, 8973 registrations, 6831 symbols and continues growing.

Example of the mizar program

The mizar libraries are built up on the base of extremely primitive mathematical objects with minimum of predetermined notation. This is the main difference from the Mathematica or Maple.

For any practical application, a lot of library definitions should be loaded before. The appropriate search for the appropriate libraries with compatible notations forms the most heavy and difficult part of the job in writing of any mizar program.

Here is an example of the mizar program that checks that 1+1=2 and 1/2-1/3=1/6:

environ
vocabularies ARYTM_1, RELAT_1, ARYTM_3, REAL_1;
notations  ORDINAL1, XCMPLX_0, XREAL_0, XXREAL_0;
constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0;
registrations ORDINAL1,NUMBERS, XREAL_0;
requirements  BOOLE, SUBSET, NUMERALS,ARITHM;
begin
1+1=2;
1/2-1/3=1/6;

All the capital names refer to the libraries that are loaded at the installation of the system. In order to be able to compare numbers more libraries should be found and listed at the header of the program. In particular, an example of a program, that checks the relation 2>1 is not yet available.

In principle, the mizar user may define all the symbols necessary by him/her self using the kernel mizar notations, but the problem of compatibility of notations with other mizar programs (that already are written and uploaded) may arise; therefore the use of already written libraries is recommended.

Any source from the MML library can be considered as a complicated example of a mizar program.