The Mizar system is one of the pioneering systems aimed at supporting mathematical proof development on a computer that have laid the groundwork for and eventually have evolved into modern interactive proof assistants. We claim that an important milestone in the development of these systems was the creation of organized libraries accumulating all previously available formalized knowledge in such a way that new works could effectively re-use all previously collected notions. In the case of Mizar, the turning point of its development was the decision to start building the Mizar Mathematical Library as a centrally-managed knowledge base maintained together with the formalization language and the verification system. In this paper we show the process of forming this library, the evolution of its design principles, and also present some data showing its current use with the modern version of the Mizar proof checker, but also as a rich corpus of semantically linked mathematical data in various areas including web-based and natural language proof presentation, maths education, and machine learning based automated theorem proving.

In this paper we present the methodology of implementing a new enhancement of the Mizar proof checker based on enabling special processing of Euclidean predicates, i.e. binary predicates which fulfill a specific variant of transitivity postulated by Euclid.Typically, every proof step in formal mathematical reasoning is associated with a formula to be proved and a list of references used to justify the formula.With the proposed enhancement, the Euclidean property of given relations can be registered during their definition, and so the verification of some proof steps related to these relations can be automated to avoid explicit referencing.

This special issue is dedicated to works related to Mizar , the theorem proving project started by Andrzej Trybulec in the 1970s, and other automated proof checking systems used for formalizing mathematics.

In this paper we present the results of an experiment with employing an external SAT solver to strengthen the notion of obviousness of the Mizar proof checker. The presented extension of the Mizar system is based on a version of MiniSAT, called Logic2CNF. The SAT-enhanced Mizar checker is programmed to automatically spawn a new Logic2CNF process whenever it needs to justify any goal that can be solved by reducing it into a corresponding propositional satisfiability problem (equalities based on Boolean operations or set inclusion). The external tool is interfaced within the implementation of Mizar ’s requirements directives.

The collection of works for this special issue was inspired by the presentations given at the 2011 AMS Special Session on Formal Mathematics for Mathematicians: Developing Large Repositories of Advanced Mathematics . The issue features a collection of articles by practitioners of formalizing proofs who share a deep interest in making computerized mathematics widely available.