MizAR 60 for Mizar 50

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…

• GA
  Grantová Agentura České Republiky

  Awards: CZ.02.1.01/0.0, CZ.02.1.01
• H2
  Horizon 2020 Framework Programme

  Awards: 952215, 857306
• ER
  European Regional Development Fund

  Awards: 02.1.01/0.0/0.0, CZ.02.1.01/0.0/0.0/15_003/0000466, H2020, CZ.02, CZ.02.1.01, CZ.02.1.01/0.0/0.0, CZ.02.1.01/0.0/0.0/