Mizar: the first usable proof assistant for mathematics

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…