Learning Systems for Interactive Theorem Proving

Abstract

Interactive theorem proving is a great tool to establish correctness of programs and mathematics. Despite the well-known undecidability of any fairly expressive system, it is possible to leverage machine learning to help find proofs in a humanlike way. This thesis focuses on interactive theorem proving (ITP) and its high-level automation. We describe our system TacticZero, which is a framework that learns ITP in an end-to-end manner without using human proofs. We further propose potential solutions to the challenges arising from TacticZero — the cut-formula problem and the problem of efficiency, and demonstrate the effectiveness of the solutions.