constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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)
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq)
Xena project (using Lean)
Historical projects that died out:
Wikipedia, Mizar system
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)