Mizar is a formal language used to write mathematical definitions and proofs that are as close as possible to vernacular. One can profit from Mizar by using it as: an integrated library (linked within itself) containing proofs generated through the protocols of Mizar; a proof checker, provided the proof is written according to Mizar syntax; or an assistant using Bayesian search to find suitable axioms or theorems that could serve as proofs.

The authors of this paper describe several aspects of these uses, concentrating mostly on the third, which is often known in computer science as an “authoring environment.” Through examples from graph theory, they show how Mizar can serve as an interactive tutorial or an assistant for constructing a proof, by finding suitable theorems.

The paper also makes some brief comparisons with other proof checkers or proof assistants, including Isabelle [1] (the Sledgehammer part).

Some concerns are expressed over the method for interacting with Mizar, either through Emacs or Hypertext Markup Language (HTML). The latter is prized for the possibility of using Extensible Markup Language (XML) to disambiguate mathematical symbols or definitions used in different areas of mathematics, with possibly different meanings.

Finally, the authors mention several problems to be worked out regarding possible links among the three uses, and with other systems, to make Mizar more efficient, and hence more attractive as a proof-checker, proof-assistant, and proof-publisher.

I recommend this paper to computer scientists working on operating systems, and mathematicians working on mathematical artificial intelligence or provability theory.