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 the command "mizf", for example,

mizf something

or

mizf something.miz

A Mizar 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 Mathematical Library (MML), included in the distribution, consists of definitions and theorems which can be referred to in a newly written program. After a program has been reviewed and checked automatically, it can be published as an article in the associated Journal of Formalized Mathematics .

As of the end of 2009, the Mizar Mathematical Library (version 4.130.1076) includes 1073 articles written by 226 authors, containing 49548 theorems, 9487 definitions, 785 schemes, 8973 registrations, 6831 symbols, and continues to grow.

Examples of a Mizar program

The Mizar libraries are built upon a base of extremely primitive mathematical objects with a minimum of predetermined notation. This is a main difference to Mathematica and Maple.

For any practical application, a lot of library definitions have to be loaded. The search for the appropriate libraries with a compatible notation forms the most exacting and difficult part of the job when writing a Mizar program.

In principle, a Mizar user may define all the symbols needed, using Mizar kernel notations, but then problems of compatibility with the notations used by other Mizar programs (that already are written and uploaded) may arise in case the program is reused by other programs; therefore the use of existing libraries is recommended.

Sum of two rational numbers

Here is an example of a Mizar program that checks if " 1 + 1 = 2 " and " 1/2 - 1/3 = 1/6 " are true:

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 uppercase names refer to a library that is loaded when the system is invoked to check the program.

Order relation

In order to be able to compare numbers, even more libraries must be found and listed in the header of the program. However, the readers of some already existing programs could be used. Below, a Mizar program that checks the relations "2 > 1", " 2 ≥ 2 " and " 2 ≥ 3 " is copypasted:

environ
vocabularies NUMBERS, RELAT_2, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, TOPREAL1,
     XXREAL_0, ARYTM_3, FINSEQ_1, JORDAN9, MATRIX_1, JORDAN8, PARTFUN1,
     RELAT_1, TREES_1, GOBOARD1, GOBOARD5, ARYTM_1, CARD_1, XBOOLE_0, TARSKI,
     RLTOPSP1, PSCOMP_1, NEWTON, MCART_1, PRE_TOPC, GOBOARD9, TOPS_1, REAL_1,
     CONNSP_1, STRUCT_0, JORDAN2C, CONNSP_3, XXREAL_2, SETFAM_1, ZFMISC_1,
     TOPREAL4, PCOMPS_1, WEIERSTR, METRIC_1, JORDAN10;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, NUMBERS, REAL_1, NAT_1, NAT_D,
     PARTFUN1, FINSEQ_1, NEWTON, DOMAIN_1, STRUCT_0, METRIC_1, TBSP_1,
     WEIERSTR, PRE_TOPC, TOPS_1, CONNSP_1, CONNSP_3, COMPTS_1, PCOMPS_1,
     MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, TOPREAL4,
     PSCOMP_1, GOBOARD9, SPPOL_1, JORDAN2C, JORDAN8, GOBRD13, TOPREAL6,
     JORDAN9, XXREAL_0;
constructors SETFAM_1, XXREAL_0, REAL_1, NAT_1, NEWTON, REALSET1, BINARITH,
     TOPS_1, CONNSP_1, TBSP_1, TOPREAL4, JORDAN1, PSCOMP_1, WEIERSTR,
     GOBOARD9, CONNSP_3, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13, JORDAN9, NAT_D,
     FUNCSDOM, CONVEX1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, MEMBERED, FINSEQ_1,
     STRUCT_0, PRE_TOPC, COMPTS_1, PCOMPS_1, EUCLID, TOPREAL1, SPPOL_2,
     SPRECT_1, SPRECT_2, JORDAN2C, TOPREAL6, JORDAN8, FUNCT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, SUBSET_1, PSCOMP_1, CONNSP_3;
theorems CONNSP_1, CONNSP_3, EUCLID, GOBOARD6, GOBOARD7, GOBOARD9, GOBRD11,
     GOBRD13, GOBRD14, JGRAPH_1, JORDAN2C, JORDAN3, JORDAN6, JORDAN8, JORDAN9,
     NEWTON, NAT_1, PRE_TOPC, SETFAM_1, SPPOL_2, SPRECT_1, SPRECT_3, SPRECT_4,
     SUBSET_1, TARSKI, TOPREAL1, TOPREAL3, TOPREAL4, TOPREAL6, TOPS_1,
     WEIERSTR, ZFMISC_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, REALSET1, XREAL_1,
     XXREAL_0, MATRIX_1, XREAL_0, COMPTS_1, RLTOPSP1;
schemes NAT_1;
begin  :: Properties of the external approximation of Jordan's curve
registration
 cluster connected compact non vertical non horizontal Subset of TOP-REAL 2;
 existence
 proof
   take R^2-unit_square;
   thus thesis;
 end;
end;
2>1;
2>=2;
2>=3;
::> *4
::>
::> 4: This inference is not accepted

In the example above, the relations "2 > 1" and " 2 ≥ 2 " are accepted. The last statement (" 2 ≥ 3 ") is false. This is recognized by the program and shown in the three last lines after this statement that are added by Mizar; they indicate that this statement is not accepted.

Perhaps, namely for the comparison of numerical constants, the size of the header can be reduced. Generally, it is difficult to guess which libraries are required to prove some given set of statements.

Some algebra

With the same header, as in the example above, the elementary algebra can be verified. Below, the header is not copypasted (although it should exist at the top of the Mizar code), but few algebraic statements are added:

 2>1;
 2>=2;
 reserve x,y,z for Real;
 (x+y)*z=x*z+y*z;
 x*y=y*x;
 x+x=2*x;
 x+y=x*y;
::>    *4
::>
::> 4: This inference is not accepted

In order to specify, that the example deals with real, the special reservation is necessary. Then, the Mizar accepts the statements $x*y=y*x$ and $x+x=2*x$, but rejects the relation $x+y=x*y$ because its value depends on values of the variables; this expression has value true for $x=2$, $y=2$ and it has value false for $x=1$, $y=1$.

Elementary functions

The elementary functions can be searched in the libraries, and require the additional names to be listed in the header. With the same headers, the result of mizaring indicates the errors, as in the example below. For example, the statement $(x+y)^{2}=x^{2}+2*x*y+y^{2}$ will not be accepted, because the operation ^ is not yet defined. In this case, the error message will be different from that above:

 (x+y)^2=x^2+2*x*y+y^2
::>   *203
::>
::> 203: Unknown token, maybe an illegal character used in an identifier

In principle, the definition of operation ^ could be found among the supplied programs, but there are thousands there, and it is difficult to check them one by one.

The same refers to other functions, the SIN_COS and some other names should be listed; over-vice, the result may look as follows:

1^1=1;
::>,203
2 < number_e;
::>        *165
3< PI ;
::> *165
exp(0)=1;
::>,148
sin(0)=0;
::>,165
::>
::> 148: Unknown private functor
::> 165: Unknown functor format
::> 203: Unknown token, maybe an illegal character used in an identifier

although the operations ^, exp, sin and the numbers PI and number_e are listed in the table of notations.

Bottle neck

The bottle neck of the Mizar seems to be the search of the appropriate libraries. In a random way, it is difficult to find the correct combination of the names in the headers. The number of possible ordered combinations is of order of 1400!, that greatly exceeds the computer facilities.