Editing Mizar system (section)

== Mizar Mathematical Library ==

The Mizar Mathematical Library (MML) includes all theorems to which authors can refer in newly written articles. Once approved by the proof checker they are further evaluated in a process of [[peer-review]] for appropriate contribution and style. If accepted they are published in the associated ''Journal of Formalized Mathematics''<ref name="Journal of Formalized Mathematics">[http://fm.mizar.org/ ''Journal of Formalized Mathematics'']</ref> and added to the MML.

=== Breadth ===

As of July 2012, the MML included 1150 articles written by 241 authors.<ref name="MML Query">[http://mmlquery.mizar.org The MML Query search engine]</ref> In aggregate, these contain more than 10,000 formal definitions of mathematical objects and about 52,000 theorems proved on these objects. More than 180 named mathematical facts have been given formal codification in this manner.<ref name="MML facts">{{cite web | title = A list of named theorems in the MML | url = http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=mml-facts.mqt&argument=number+102 | accessdate = 22 July 2012}}</ref> Some examples are the [[Hahn–Banach theorem]], [[Kőnig's lemma]], the [[Brouwer fixed point theorem]], [[Gödel's completeness theorem]], and the [[Jordan curve theorem]].

This breadth of coverage has led some<ref>{{cite journal | last = Wiedijk | first = Freek | title = The QED Manifesto Revisited | journal = From Insight to Proof: Festschrift in Honour of Andrzej Trybulec | year = 2007 | volume = 10 | series = [[Studies in Logic, Grammar and Rhetoric]] | issue = 23 | url = https://www.cs.ru.nl/~freek/pubs/qed2.pdf}}</ref> to suggest Mizar as one of the leading approximations to the [[QED manifesto|QED utopia]] of encoding all core mathematics in computer verifiable form.

=== 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>

=== Logical structure ===

The MML is built on the axioms of the [[Tarski–Grothendieck set theory]]. Even though semantically [[implementation of mathematics in set theory|all objects are sets]], the language allows one to define and use [[weak typing|syntactical weak types]]. For example, a set may be declared to be of type '''Nat''' only when its internal structure conforms with a particular list of requirements. In turn, this list serves as the definition of the [[natural numbers]] and the set of all the sets that conform to this list is denoted as '''NAT'''.<ref>{{cite journal | last = Grabowski | first = Adam |author2=Artur Kornilowicz |author3=Adam Naumowicz  | title = Mizar in a Nutshell | journal = [[Journal of Formalized Reasoning]] | year = 2010 | volume = 3 | issue = 2 | pages = 152–245 | url = http://jfr.unibo.it/article/view/1980}}</ref> This implementation of types seeks to reflect the way most mathematicians formally think of symbols<ref>{{cite book | last = Taylor | first = Paul | title = Practical Foundations of Mathematics | year = 1999 | publisher = [[Cambridge University Press]] | isbn = 9780521631075 | url = http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/ | access-date = 2012-07-24 | archive-url = https://web.archive.org/web/20150623031212/http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/ | archive-date = 2015-06-23 | url-status = dead }}</ref> and so streamline codification.