Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract)

Premise selection is a key component for the Sledgehammer tool which lets the user of a proof assistant use automated theorem provers. The Isabelle proof assistant includes several premise selection algorithms: MePo, MaSh Naive Bayes, MaSh k-Nearest Neighbors, and MeSh. Lean 4 does not currently provide a Sledgehammer, nor does it have an implementation of the premise selection algorithms necessary for a Sledgehammer implementation. By implementing premise selection algorithms, a Sledgehammer can be developed for Lean 4. Isabelle's premise selection algorithms are ported to Lean 4 and the necessary infrastructure is developed. Performance of the algorithms is evaluated and compared to their Isabelle counterparts using the original research that produced the MaSh and MeSh premise selection algorithms. Performance of the MaSh NB, MaSh k-NN, and MeSh algorithms in Lean 4 is comparable to their Isabelle counterparts. The MePo algorithm does not achieve comparable performance, however, because of differences between the experiment and its Isabelle counterpart. Most of the ported algorithms can be successfully used to perform premise selection in Lean 4. When a Sledgehammer is implemented for Lean 4, realworld performance of the premise selection algorithms can be measured.