Mizar System - Mizar Language

Mizar Language

The distinctive feature of the Mizar language is its readability. As is common in mathematical text, it relies on classical logic and a declarative style. Mizar articles are written in ordinary ASCII, but the language was designed to be close enough to the mathematical vernacular that most mathematicians could read and understand Mizar articles without special training. Yet, the language enables the increased level of formality necessary for automated proof checking.

For a proof to be admitted, all steps have to be justified either by elementary logical arguments or by citing previously verified proofs. This results in a higher level of rigor and detail than customary in mathematical text-books and publications. Thus, a typical Mizar article is about four times as long as an equivalent paper written in ordinary style.

Formalization is relatively labor intensive, but not impossibly difficult. Once one is versed in the system, it takes about one week of full-time work to have a text-book page formally verified. This suggests that its benefits are now in the reach of applied fields such as probability theory and economics.