In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above 80\%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar,and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14\% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3021 (21.3\%) of the 14163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.

翻译：本工作中，我们通过结合多种自动定理证明与人工智能方法，证明了超过3000个先前未被ATP证明的Mizar/MPTP问题，将ATP可解的Mizar问题比例从75%提升至80%以上。首先，我们开始实验采用cvc5 SMT求解器，该求解器运用了多种基于实例化的启发式策略，这与先前应用于Mizar的基于超位置的系统不同，从而带来了大量新的解。随后，我们通过自动化策略发明来开发cvc5策略，这些策略显著提升了cvc5在困难问题上的性能。特别地，最优发明策略比先前可用的最优cvc5策略多解决了超过14%的问题。我们还证明了不同的子句化方法对此类基于实例化的方法具有重要影响，再次产生了许多新的解。总体而言，这些方法在14163个先前未解决的困难Mizar问题中解决了3021个（占21.3%）。这是Mizar大理论基准测试的新里程碑，也是对Mizar的“锤子”方法的重要加强。