Editing Mizar system (section)

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