Editing Mizar system (section)

=== Availability ===

All MML articles are available in [[PDF]] form as the papers of the ''Journal of Formalized Mathematics''.<ref name="Journal of Formalized Mathematics"/> The full text of the MML is distributed with the Mizar checker and can be freely downloaded from the Mizar website. In an ongoing recent project<ref>[https://archive.today/20130222164311/http://foundations.cs.ru.nl/fndswiki/Research/MathWiki The MathWiki project homepage]</ref> the library was also made available in an experimental [[wiki]] form<ref name="MML wiki">[https://web.archive.org/web/20131202235227/http://mws.cs.ru.nl/mwiki/ The MML in wiki form]</ref> that only admits edits when they are approved by the Mizar checker.<ref>{{cite conference
 | last1 = Alama | first1 = Jesse
 | last2 = Brink | first2 = Kasper
 | last3 = Mamane | first3 = Lionel
 | last4 = Urban | first4 = Josef
 | editor1-last = Davenport | editor1-first = James H.
 | editor2-last = Farmer | editor2-first = William M.
 | editor3-last = Urban | editor3-first = Josef
 | editor4-last = Rabe | editor4-first = Florian
 | arxiv = 1107.3209
 | contribution = Large Formal Wikis: Issues and Solutions
 | doi = 10.1007/978-3-642-22673-1_10
 | pages = 133–148
 | publisher = Springer
 | series = Lecture Notes in Computer Science
 | title = Intelligent Computer Mathematics – 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings
 | volume = 6824
 | year = 2011| isbn = 978-3-642-22672-4
 }}</ref>

The MML Query website<ref name="MML Query"/> implements a powerful search engine for the contents of the MML. Among other abilities, it can retrieve all MML theorems proved about any particular type or operator.<ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(symbol+to_power+|+notation+|+constructor+|+occur+|+th)+ordered+by+number+of+ref An example of an MML query], yielding all theorems proved on the [[exponent]] operator, by the number of times they are cited in subsequent theorems.</ref><ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(atleast+*+(+PROB_1:modenot+3+ref)+%7C+th)+ordered+by+number+of+ref Another example of an MML query], yielding all theorems proved on [[sigma field]]s.</ref>