Result: Learning-Assisted Reasoning within Proof Assistants via Symbolic, Statistical, and Neural Guidance

Proof assistants, developed within the field of Interactive Theorem Proving (ITP), provide mathematicians with tools to construct proofs that can be rigorously verified by computers. This capability is particularly valuable given the extreme complexity of contemporary mathematics. However, the manual development of proofs in ITP systems is significantly more time-intensive compared to traditional handwritten proofs. One promising approach to mitigating these difficulties involves the application of machine learning techniques to automate proof construction in ITP systems. Despite recent breakthroughs in machine learning across various fields, the domain of mathematical reasoning still presents formidable challenges. This dissertation aims to leverage a range of machine learning methods to enhance proof automation within ITP environments. To address this goal, my research centers on devising innovative feature representations and implementing diverse learning models specifically designed to enhance the prediction accuracy of proof steps within ITP. Furthermore, I investigate a new task, referred to as proof transformation learning, which is highly relevant to proof automation. Instead of predicting the next proof step solely relying on the proof state before its application, proof transformation learning utilizes both the proof states before and after the proof step to make predictions. I also explore the first application of inductive logic programming in deriving rules that predict when specific proof steps are appropriate within the context of ITP.