TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

Minchao Wu, Michael Norrish, Christian Walder +1

We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tacti…