Mizar system

The Mizar system combines three things: a formal language for writing mathematical definitions and proofs, a proof assistant that mechanically checks proofs written in that language, and a library of formalized mathematics that new proofs can build on. The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct the vernacular of mathematics so that a computer could check it. It is now developed by research groups at Bialystok University in Poland, the University of Alberta in Canada and Shinshu University in Japan. The language is distinctive for its readability: it relies on classical logic and a declarative style, is written in plain ASCII and is close enough to ordinary mathematical text that most mathematicians can read it. Every step of a proof must be justified by elementary logic or by citing a verified result. The Mizar Mathematical Library, whose articles are peer reviewed and published in the Journal of Formalized Mathematics, held 1150 articles by 241 authors as of July 2012. The proof checker is proprietary while the library is open source.