Editing Mizar system (section)

{{for|the star system|Mizar (star)}}
{{Infobox programming language
 | name                   = Mizar
 | logo                   = [[File:Mizar system logo.gif]]
 | logo caption           = 
 | screenshot             = Mizar MathWiki screenshot.png
 | collapsible = yes
 | screenshot caption     = Mizar MathWiki screenshot
 | file ext               = .miz .voc
 | paradigm               = [[Declarative programming|Declarative]]
 | scope                  =
 | released               = 1973
 | designer               =  [[Andrzej Trybulec]]
 | developer              = 
 | latest release version = 
 | latest release date    = <!-- {{start date and age|YYYY|MM|DD}} -->
 | latest preview version = 
 | latest preview date    = <!-- {{start date and age|YYYY|MM|DD}} -->
 | typing                 = [[Weak typing|Weak]], [[Static typing|static]]
 | implementations        = 
 | dialects               = 
 | influenced by          = [[Automath]]
 | influenced             = [[OMDoc]], [[HOL Light]] and [[Coq (software)|Coq]] mizar modes
 | programming language   = 
 | platform               = 
 | operating system       = 
 | license                = 
 | website                = [http://mizar.uwb.edu.pl/ www.mizar.org]
 | wikibooks              = 
}}

The '''Mizar system''' consists of a [[formal language]] for writing mathematical definitions and proofs, a [[proof assistant]], which is able to [[Automated proof checking|mechanically check]] proofs written in this language, and a library of [[mathematical formalization|formalized mathematics]], which can be used in the proof of new theorems.<ref name="A Brief Overview of Mizar">{{cite conference
 | last1 = Naumowicz | first1 = Adam
 | last2 = Kornilowicz | first2 = Artur
 | editor1-last = Berghofer | editor1-first = Stefan
 | editor2-last = Nipkow | editor2-first = Tobias
 | editor3-last = Urban | editor3-first = Christian
 | editor4-last = Wenzel | editor4-first = Makarius
 | contribution = A Brief Overview of Mizar
 | doi = 10.1007/978-3-642-03359-9_5
 | pages = 67–72
 | publisher = Springer
 | series = Lecture Notes in Computer Science
 | title = Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17–20, 2009. Proceedings
 | volume = 5674
 | year = 2009| isbn = 978-3-642-03358-2
 }}</ref> The system is maintained and developed by the Mizar Project, formerly under the direction of its founder [[Andrzej Trybulec]].

In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.<ref name="Arrow">{{cite journal | last = Wiedijk | first = Freek | title = Formalizing Arrow's theorem | journal = [[Sādhanā (journal)|Sādhanā]] | year = 2009 | volume = 34 | pages = 193–220 | issue = 1 | doi=10.1007/s12046-009-0005-1| hdl = 2066/75428 | doi-access = free | hdl-access = free }}</ref>