Mizar: the first usable proof assistant for mathematics

Machine Logic

At the junction of computation, logic and mathematics

Mizar: the first usable proof assistant for mathematics

07 May 2026

memories

Mizar

AUTOMATH

Isar

In two recent blogposts I have outlined the history of our field,<br>one on the history of proof assistants and another specifically about earlier work on the<br>formalisation of mathematics by machine.<br>And yet, bizarrely, I overlooked one of the earliest<br>and most influential proof assistants for mathematics: Mizar.<br>Here, to make amends, are a few words on Mizar and its influence on our field.<br>I only wish I were better qualified to tell the story.

Origins, or, utterly different from AUTOMATH

Mizar was created by Andrzej Trybulec of Białystok University, Poland and was designed<br>from the start to accept a language close to ordinary mathematical writing.<br>As the project developed, team members (Piotr Rudnicki, Grzegorz Bancerek and many others)<br>eventually decided to create a library of contributions:<br>the Mizar Mathematical Library.<br>The MML already held an impressive collection of formal mathematics 30 years ago.<br>With Europe divided by the Iron Curtain until 1989,<br>Mizar escaped the notice of Western researchers.<br>But after the launch of the<br>QED Manifesto in 1993,<br>which proposed the goal of formalising all known mathematics by computer,<br>its Western organisers suddenly did notice the outstanding progress made by Mizar and MML,<br>which had been going on quietly for decades.<br>Suddenly, Mizar was at the centre of the QED project.

As I’ve described many times, AUTOMATH<br>arose in the 1960s,<br>based on the idea that the elements of mathematical reasoning<br>(truth values and functions, hence typed sets and sequences, etc)<br>can be reduced to a simple extended λ-calculus.<br>De Bruijn was not concerned about capturing the style of mathematical writing.<br>Instead, he set out to isolate the minimum core needed to express mathematics.<br>Mizar instead focused on capturing mathematical writing in all its<br>richness, aiming to be as natural as possible while being formal.<br>Again we see the benefit of a plurality of approaches.

Cold War realities

The differences between AUTOMATH and Mizar are striking.<br>This extreme divergence is likely due to the Cold War.<br>People younger than 50 may find it hard to grasp the realities of that time.<br>You could hitchhike from Amsterdam to Munich easily enough,<br>but Leipzig might as well have been on Mars and Białystok was<br>practically at the Soviet border.<br>People who lived in the East could not easily travel to the West<br>to exchange ideas at conferences.<br>Westerners could travel to the East, though with some difficulty,<br>and the FBI or MI5 would probably open a file on you.<br>Hardly anyone made the effort; a notable exception was Tony Hoare.<br>Few ideas crossed the divide.

We had some visitors from the Polish Academy of Sciences in the mid 1980s;<br>apparently they had been “invited” to leave due to their pro-Solidarity activism.<br>One of them, Stefan Sokołowski, devised a way<br>to integrate unification and backtracking search into LCF;<br>his ideas had a strong impact on Isabelle,<br>where unification and backtracking are also built-in.<br>Another was Andrzej Tarlecki and yet another was Andrzej Blikle,<br>who in addition to his scientific work ran the famous bakery in Warsaw.

The International Conference on Computer Logic,<br>was held in Tallinn in 1988.<br>Organised by Per Martin-Löf and Grigori Mints, this event<br>brought Western and Soviet researchers together mostly for the first time.<br>Its very existence was a sign of thawing relations;<br>the Berlin Wall came down only a year later.

Noteworthy features

One difficult aspect of mathematical vernacular is how it lets<br>you mix and match properties of abstract entities:<br>finite abelian groups; complete distributive lattices<br>Moreover, some properties imply others, e.g. a cyclic group is necessarily abelian.<br>Mizar provides an elaborate system of attributes<br>to manage such properties. This sort of reasoning is pervasive in mathematics,<br>and I think that Mizar does it more naturally<br>than any other proof assistant.

Mizar implements a strong version of set theory (Tarski-Grothendieck),<br>making it equivalent in logical strength to Lean and Rocq.1<br>But while the latter two implement the calculus of inductive constructions,<br>a dependent-typed theory, Mizar builds a “soft” type system on its set theoretical foundation.<br>Some sort of typed language is definitely necessary for doing mathematics:<br>you can’t get very far if you have to worry about whether 5 happens to be a group.<br>Below the type system, you have classical first order logic.<br>There are no “proof tactics” but rather a built-in prover that justifies proof lines.<br>It is based on a notion of “obvious inferences”<br>that is designed to offer some automation but with a guarantee of termination.

Impacts

The influence of Mizar is visible everywhere in today’s proof assistant ecosystem.<br>Above all, people are starting to recognise the...