Abstract

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.

BibTeX

@inproceedings{jjkczgckmobpssmsju-itp23,
  author       = {Jan Jakubuv and
                  Karel Chvalovsk{\'{y}} and
                  Zarathustra Amadeus Goertzel and
                  Cezary Kaliszyk and
                  Mirek Ols{\'{a}}k and
                  Bartosz Piotrowski and
                  Stephan Schulz and
                  Martin Suda and
                  Josef Urban},
  editor       = {Adam Naumowicz and Ren{\'{e}} Thiemann},
  title        = {{MizAR} 60 for {M}izar 50},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP} 2023},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {19:1--19:22},
  publisher    = {Schloss Dagstuhl},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.19},
  doi          = {10.4230/LIPICS.ITP.2023.19},
}