MizAR 60 for Mizar 50

   Jan Jakubuv, Karel Chvalovsky, Zarathustra Goertzel,
   Cezary Kaliszyk, Mirek Olsak, Bartosz Piotrowski,
   Stephan Schulz, Martin Suda, and Josef Urban

As a present to Mizar on its 50th anniversary, we develop an AI/TP
system that automatically proves about 60 % of the Mizar theorems in
the hammer setting. We also automatically prove 75 % of the Mizar
theorems when the automated provers are helped by using only the
premises used in the human-written Mizar proofs. We describe the
methods and large-scale experiments leading to these results. This
includes in particular the E and Vampire provers, their ENIGMA and
Deepire learning modifications, a number of learning-based premise
selection methods, and the incremental loop that interleaves growing a
corpus of millions of ATP proofs with training increasingly strong
AI/TP systems on them. We also present a selection of Mizar problems
that were proved automatically.