[2] The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct mathematical vernacular so it can be checked by a computer.

[3] Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics.

[6] Papers related to the Mizar system regularly appear in the peer-reviewed journals of the mathematic formalization academic community.

Thus, a typical Mizar article is about four times as long as an equivalent paper written in ordinary style.

Once one is versed in the system, it takes about one week of full-time work to have a textbook page formally verified.

[2] The Mizar Mathematical Library (MML) includes all theorems to which authors can refer in newly written articles.

This breadth of coverage has led some[13] to suggest Mizar as one of the leading approximations to the QED utopia of encoding all core mathematics in computer verifiable form.

In an ongoing recent project[14] the library was also made available in an experimental wiki form[15] that only admits edits when they are approved by the Mizar checker.