Mizar is a language designed by A. Trybulec in the early seventies in order to represent mathematical proof in the computer. And the Mizar project (in Bialystok, Poland) is still quite active. Mizar is currently the best approximation available to the QED dream of encoding real mathematics for digital proof checking. I think.
The Mizar project has its own website, which is the official source of Mizar files. However, there's also a site about Mizar by Piotr Rudnicki (which includes a mirror of the Polish site as well) that once I thought was a bit better. Also: apart from the group in Bialystok there's another big Mizar effort going on in Japan.
The closest thing to a Mizar manual (although it is obsolete and for me it is not very easy to understand) is An Outline of PC Mizar by Michal Muzalewski from 1993 (this is gzipped postscript; there also is a dvi version.) This text is owned by the Mizar Users Group although the electronic version may be distributed freely.
Mizar is usually used under DOS/Windows, but it has been ported to Linux too. There is an emacs mode for Mizar which is quite nice.
To give an impression of the Mizar language, here's a small proof in it:
theorem Th2: ex x, y st x is irrational & y is irrational & x.^.y is rational proof set w = sqrt 2; A1: w is irrational by INT_2:44,Th1; w>0 by AXIOMS:22,SQUARE_1:84; then A2: (w.^.w).^.w = w.^.(w * w) by POWER:38 .= w.^.(w^2) by SQUARE_1:def 3 .= w.^.2 by SQUARE_1:def 4 .= w^2 by POWER:53 .= 2 by SQUARE_1:def 4; per cases; suppose A3: w.^.w is rational; take w, w; thus thesis by A1,A3; suppose A4: w.^.w is irrational; take w.^.w, w; thus thesis by A1,A2,A4,RAT_1:7; end;
In this proof the label "Th1" in the sixth line refers to the theorem that:
theorem Th1: p is prime implies sqrt p is irrational;
The other references all are to the "MML" (which stands for "Mizar Mathematical Library"), the gigantic library that accompanies the system (at the time of writing is was 49 megabytes with proofs, and 7 megabytes without.)
In July 1999 I visited Poland to learn Mizar. This was a pleasant experience: the system turned out to be wonderful, Poland was lovely, and the Mizar people were very hospitable. I highly recommend everyone to pay the Mizar project a visit like that.
While working on Mizar I created:
I haven't decided yet wether I'll be going to continue to put work into learning and using Mizar (and if so: what I'll be going to do), but I think it might be a good idea.
(last modification 2002-01-29)