  We propose a novel approach to interactive theorem-proving (ITP) using deep
reinforcement learning. Unlike previous work, our framework is able to prove
theorems both end-to-end and from scratch (i.e., without relying on example
proofs from human experts). We formulate the process of ITP as a Markov
decision process (MDP) in which each state represents a set of potential
derivation paths. The agent learns to select promising derivations as well as
appropriate tactics within each derivation using deep policy gradients. This
structure allows us to introduce a novel backtracking mechanism which enables
the agent to efficiently discard (predicted) dead-end derivations and restart
the derivation from promising alternatives. Experimental results show that the
framework provides comparable performance to that of the approaches that use
human experts, and that it is also capable of proving theorems that it has
never seen during training. We further elaborate the role of each component of
the framework using ablation studies.
