Mizar

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:

a talk about Mizar for the Fifth Dutch Proof Tools Day in Ghent
a version of the Mizar syntax which is more compact and therefore (to me) more readable than the one that's available on the Mizar site: it's a handy reference to the language
an attempt at an introduction to Mizar: a 42 page note called Mizar: An Impression (this is gzipped postscript; there also are dvi and tex versions)
another attempt at an introduction to Mizar: a tutorial called Writing a Mizar article in nine easy steps (this is gzipped postscript: there also are dvi and pdf versions)
a compilation of a number of e-mail messages that Andrzej Trybulec sent to me explaining the basic inference step ("by") of Mizar (this is gzipped postscript; there also are dvi and tex versions)
a few wishes I have for the Mizar system (this is gzipped postscript; there also are dvi and tex versions)
an investigation of the de Bruijn factor of (among other formalizations) two Mizar articles
a Mizar development about the irrationality of e: its 42 lemmas (beware of the high ascii), its abstract (the same file without proofs), and its disturbing voc file
a graph of the Mizar library generated using ocamldot (this is gzipped postscript; there also is a huge gif version)
a font (which I also called "Mizar") for the Mac that shows high ascii in DOS encoding: when Mizar still used high ascii characters this used to be necessary to read Mizar files on the Mac (it's a nine point screen font in the tradition of Monaco and Mishawaka.) I also converted this font for use under X

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)