Mizar: the first usable proof assistant for mathematics

This blog post details the history and impact of Mizar, one of the earliest proof assistants for mathematics, created by Andrzej Trybulec. It highlights Mizar's unique features, such as its accessible language structure and the extensive Mizar Mathematical Library, contrasting it with other systems like AUTOMATH. The piece discusses the influence of political circumstances on mathematical collaboration and acknowledges Mizar's role in the evolution of proof assistants. The author reflects on Poland's contributions to mathematics, especially under challenging historical conditions.