Jan Jakubův, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
14th International Conference on Interactive Theorem Proving, pp. 19:1-19:22, 2023.
pdf 
doi:10.4230/LIPIcs.ITP.2023.19
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},}