Mizar in nLab

Contents

Contents

Idea

Mizar is a proof assistant system. It is based on Tarski–Grothendieck set theory (rather than type theory as systems such as Coq or Agda). Presently Mizar stands out among other proof assistants by the large size of its library of formalized mathematics. On the other hand, the formal proof of research-level theorems in Mizar remains a challenge :

One of the biggest problems that worry the developers of automated deduction systems is that their systems are not sufficiently recognized and exploited by working mathematicians. Unlike the computer algebra systems, the use of which has indeed become ubiquitous in the work of mathematicians these days, deduction systems are still seldom used. They are mostly used to formalize proofs of well-established and widely known classical theorems, the Fundamental Theorem of Algebra formalized in the systems Coq and Mizar may serve as a perfect example here. Such work, however, is not always considered to be really challenging from the viewpoint of mathematicians who are concerned with obtaining their own new results. Therefore it has been recognized as a big challenge for the deduction systems community to prove that some of the state-of-the-art systems are developed enough to cope with formalizing recent mathematics. (Naumowicz 06)

References

• Wikipedia, Mizar system

• Freek Wiedijk, Mizar

• Adam Naumowicz, An example of formalizing recent mathematical results in Mizar, Journal of Applied Logic Volume 4, Issue 4, December 2006, Pages 396–413 Towards Computer Aided Mathematics (publisher)