Editing Mizar system (section)

== History ==

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.<ref>{{cite journal | last = Matuszewski | first = Roman |author2=Piotr Rudnicki | title = Mizar: the first 30 years | journal = Mechanized Mathematics and Its Applications | year = 2005 | volume = 4 | url = http://mizar.org/people/romat/MatRud2005.pdf}}</ref> 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. This is in line with the influential [[QED manifesto]].<ref>{{cite web | last = Wiedijk | first = Freek | title = Mizar | url = https://www.cs.ru.nl/~freek/mizar/ | accessdate = 24 July 2018}}</ref>

Currently the project is developed and maintained by research groups at [[Białystok University]], Poland, the [[University of Alberta]], Canada, and [[Shinshu University]], Japan. While the Mizar proof checker remains proprietary,<ref name="not-open-source">[http://old.nabble.com/TPHOLs-becomes-ITP-%28fwd%29-td19435554.html#a19493250 Mailing list discussion] {{webarchive|url=https://web.archive.org/web/20111009115553/http://old.nabble.com/TPHOLs-becomes-ITP-(fwd)-td19435554.html |date=2011-10-09 }} referring to the close-sourcing of Mizar.</ref> the Mizar Mathematical Library—the sizable body of formalized mathematics that it verified—is licensed open-source.<ref name="library-open-source">[http://mizar.uwb.edu.pl/forum/archive/1104/msg00000.html Mailing list announcement] referring to the open-sourcing of MML.</ref>

Papers related to the Mizar system regularly appear in the peer-reviewed journals of the mathematic formalization academic community. These include ''[[Studies in Logic, Grammar and Rhetoric]]'', ''Intelligent Computer Mathematics'', ''[[Interactive Theorem Proving]]'', ''[[Journal of Automated Reasoning]]'' and the ''[[Journal of Formalized Reasoning]]''.