HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover

Interactive theorem provers have emerged as powerful tools for formal verification, aiding in the rigorous verification of mathematical proofs and software correctness. However, the process of constructing and manipulating proofs within these systems can be complex and labor-intensive, often requiring significant expertise and time investment. In this work, we explore the integration of deep learning techniques to assist users of interactive theorem provers by recommending proof steps, aiming to enhance their productivity and efficiency. We develop a tailored tool designed to assist users of the HOL4 theorem prover, providing expert recommendations on the best tactics to employ based on the current state of a proof using a transformer-based model.