  We introduce a theorem proving algorithm that uses practically no domain
heuristics for guiding its connection-style proof search. Instead, it runs many
Monte-Carlo simulations guided by reinforcement learning from previous proof
attempts. We produce several versions of the prover, parameterized by different
learning and guiding algorithms. The strongest version of the system is trained
on a large corpus of mathematical problems and evaluated on previously unseen
problems. The trained system solves within the same number of inferences over
40% more problems than a baseline prover, which is an unusually high
improvement in this hard AI domain. To our knowledge this is the first time
reinforcement learning has been convincingly applied to solving general
mathematical problems on a large scale.
