Machine Logic

Mizar: the first usable proof assistant for mathematics

07 May 2026

In two recent blogposts I have outlined the history of our field, one on the history of proof assistants and another specifically about earlier work on the formalisation of mathematics by machine. And yet, bizarrely, I overlooked one of the earliest and most influential proof assistants for mathematics: Mizar. Here, to make amends, are a few words on Mizar and its influence on our field. 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 from the start to accept a language close to ordinary mathematical writing. As the project developed, team members (Piotr Rudnicki, Grzegorz Bancerek and many others) eventually decided to create a library of contributions: the Mizar Mathematical Library. The MML already held an impressive collection of formal mathematics 30 years ago. With Europe divided by the Iron Curtain until 1989, Mizar escaped the notice of Western researchers. But after the launch of the QED Manifesto in 1993, which proposed the goal of formalising all known mathematics by computer, its Western organisers suddenly did notice the outstanding progress made by Mizar and MML, which had been going on quietly for decades. Suddenly, Mizar was at the centre of the QED project.

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

Cold War realities

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

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

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

Noteworthy features

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

Mizar implements a strong version of set theory (Tarski-Grothendieck), making it equivalent in logical strength to Lean and Rocq. But while the latter two implement the calculus of inductive constructions, a dependent-typed theory, Mizar builds a “soft” type system on its set theoretical foundation. Some sort of typed language is definitely necessary for doing mathematics: you can’t get very far if you have to worry about whether 5 happens to be a group. Below the type system, you have classical first order logic. There are no “proof tactics” but rather a built-in prover that justifies proof lines. It is based on a notion of “obvious inferences” 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. Above all, people are starting to recognise the importance of a readable proof language. Isabelle’s Isar language follows Mizar in allowing declarative proofs with nested scopes. This style is also available in Lean, and to a lesser extent in other systems, though it is too seldom used. Patrick Massot has written of the importance of having proofs that we can learn from.

The Mizar Mathematical Library attempted to demonstrate that significant mathematics could be formalised and that entries could be built upon one another. The MML was recognised as an achievement 30 years ago, so other proof assistants have launched their own mathematical libraries, such as Isabelle’s AFP and Lean’s mathlib.

Looking to the future, there is even a project to emulate Mizar within Isabelle. One can only wish them success!

Postscript

Once again, I apologise for overlooking Mizar. Unfortunately, Poles have got used to being overlooked. Few in the West remember that they were the ones to finally capture Monte Cassino in the brutal Italian campaign of WWII, or that they were the first to break into the Enigma cipher, or even that Frédéric Chopin and Marie Curie were Polish. Their country disappeared from the map between 1795 and 1918. In 1939 they were invaded and in 1945, after unimaginable death and destruction, they found themselves on the wrong side of the Iron Curtain (although, according to one of our visitors, in “the happiest barracks in the Camp”). But today, Poland is doing well, and Białystok in 2023 hosted ITP (Interactive Theorem Proving) to celebrate Mizar’s 50th anniversary

I think it was Stephan who told me that one day they had been issued some Soviet-built PDP-11 clones with unreliable memory. The PDP-11 was a lovely little machine, but underpowered for such work and 10 years out of date. The achievements of Polish researchers under such conditions are truly remarkable.