Mizar is a proof-checking system used to build the Mizar Mathematical Library (MML) - a long term project aiming at building a comprehensive library of formalized mathematical knowledge.

The main goal for the design of Mizar (an effort led by Dr. Andrzej Trybulec) has been to create a formal system close to the mathematical vernacular used in main-stream mathematical publications. An additional requirement was that the language be simple enough to enable computerized processing, in particular mechanical verification of correctness. The continual development of Mizar has resulted in a language, software for checking the correctness of texts written in it, numerous utility programs, a centrally maintained library of mathematics, all of which are available on the Internet (http://mizar.org). The logic of Mizar is classical, the proofs are written in a natural deduction style and like almost all of mathematics it is based on ZF set theory beefed up with axiom of arbitrarily large, strongly inaccessible cardinals. Mizar definitions allow to introduce new constructors for types, algebraic structures, terms, adjectives, and atomic formulae. The Mizar language and the checking software evolve; the evolution is driven by the growing library. This talk offers a general information on the Mizar system, its history, its current state and its future.

One of recent activities in Mizar focuses on using automated theorem proving (ATP) systems for supporting Mizar authors. The selection of relevant premises for proving a goal is done through simple machine learning techniques (naive Bayes) but the results are helpful and encourage looking for more sophisticated ML methods.