 | |
Screenshot  Mizar MathWiki screenshot | |
| Paradigm | Declarative |
|---|---|
| Designed by | Andrzej Trybulec |
| First appeared | 1973 |
| Typing discipline | Weak, static |
| Filename extensions | .miz .voc |
| Website | www.mizar.org |
| Influenced by | |
| Automath | |
| Influenced | |
| OMDoc, HOL Light and Coq mizar modes | |
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems.[1] 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.[2]
- ^ Naumowicz, Adam; Kornilowicz, Artur (2009). "A Brief Overview of Mizar". In Berghofer, Stefan; Nipkow, Tobias; Urban, Christian; Wenzel, Makarius (eds.). Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17–20, 2009. Proceedings. Lecture Notes in Computer Science. Vol. 5674. Springer. pp. 67–72. doi:10.1007/978-3-642-03359-9_5.
- ^ Wiedijk, Freek (2009). "Formalizing Arrow's theorem". Sādhanā. 34 (1): 193–220. doi:10.1007/s12046-009-0005-1. hdl:2066/75428.