MizAR 40 for Mizar 40
  As a present to Mizar on its 40th anniversary, we develop an AI/ATP system
that in 30 seconds of real time on a 14-CPU machine automatically proves 40% of
the theorems in the latest official version of the Mizar Mathematical Library
(MML). This is a considerable improvement over previous performance of large-
theory AI/ATP methods measured on the whole MML. To achieve that, a large suite
of AI/ATP methods is employed and further developed. We implement the most
useful methods efficiently, to scale them to the 150000 formulas in MML. This
reduces the training times over the corpus to 1-3 seconds, allowing a simple
practical deployment of the methods in the online automated reasoning service
for the Mizar users (MizAR).
