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 the paper we describe a formalization of the notion of a nominative data with simple names and complex values in the Mizar proof assistant.Such data can be considered as a partial variable assignment which allows arbitrarily deep nesting and can be useful for formalizing semantics of programs that operate in real time environment and/or process complex data structures and for reasoning about the behavior of such programs.

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.

Mathematics, especially algebra, uses plenty of structures: groups, rings, integral domains, fields, vector spaces to name a few of the most basic ones.Classes of structures are closely connected -usually by inclusion -naturally leading to hierarchies that has been reproduced in different forms in different mathematical repositories.In this paper we give a brief overview of some existing algebraic hierarchies and report on the latest developments in the Mizar computerized proof assistant system.In particular we present a detailed algebraic hierarchy that has been defined in Mizar and discuss extensions of the hierarchy towards more involved domains.Taking fully formal approach into account we meet new difficulties comparing with its informal mathematical framework.

Equality is fundamental notion of logic and mathematics as a whole.If computer-supported formalization of knowledge is taken into account, sooner or later one should precisely declare the intended meaning/interpretation of the primitive predicate symbol of equality.In the paper we draw some issues how computerized proof-assistants can deal with this notion, and at the same time, we propose solutions, which are not contradictory with mathematical tradition and readability of source code.Our discussion is illustrated with examples taken from the implementation of the MIZAR system.

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.

The Mizar Verifier uses definitional expansions for controlling proof structures. In this paper we propose another use of definitional expansions—enriching verified inferences by expansions of definitions of formulae included in the inferences and increasing the number of premises accessible by Checker. This introduces more knowledge to the reasoning, which helps to draw more conclusions. Some statistics about influence of such expansions on the Mizar Mathematical Library are presented.

This paper presents some tentative experiments in using a special case of rewriting rules in Mizar (Mizar homepage: http://www.mizar.org/ ): rewriting a term as its subterm. A similar technique, but based on another Mizar mechanism called functor identification (Korniłowicz 2009) was used by Caminati, in his paper on basic first-order model theory in Mizar (Caminati, J Form Reason 3(1):49–77, 2010, Form Math 19(3):157–169, 2011). However for this purpose he was obligated to introduce some artificial functors. The mechanism presented in the present paper looks promising and fits the Mizar paradigm.

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.