We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited humanwritten theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach significantly improves the theorem prover and advances the state of the art of automated theorem proving in Metamath.
This paper focuses on the problem of developing deep learning systems that can prove theorems in a mathematical formalism -- in this case, MetaMath. This has been a rapidly growing topic in the past few years, as evidenced by the numerous cited works. What sets this work apart from others is its focus on the instrumental task of generating data to train a prover, rather than directly training the prover on human theorems (via reinforcement learning) or human proofs (via imitation learning).
The paper proposer two approaches to generating theorems imitation learning (IL) and reinforcement learning (RL). The IL approach trains a neural policy to imitate the same steps taken in human proofs. The RL approach first trains a language model on human theorems (not proofs), and uses the likelihood under the model as a reward function for an RL agent which must take forward proof steps.
Both approaches result in a policy that can be used to take proof steps, with the goal of producing new theorems which are similar to the human ones. Since the proof steps are known for the generated theorems, a prover agent (which operates in backwards mode, working from the goal back to the hypotheses) can be trained to imitate the steps taken in the synthetic proofs (along with the human ones, if any are present).
At test time, the learned prover imitation policy is then used to guide an MCTS agent, as described in the Holophrasm paper. It is compared against the original Holophrasm algorithm, rerun on modern hardware.
This is to my knowledge a novel approach in the neural theorem proving domain, and in my opinion one that offers a potentially significant advantage over the existing fixed-dataset appraoches.
The main result of the paper is that an extra 35/2720 (1.2%) of the test theorems are proven, a 6% improvement over the Holophrasm baseline of 539. It is difficult to judge how relevant of an improvement this is, and there is no analysis of the difficulty of the MetaMath problem set. In addition, due to the 10-1-1 train-validation-test split, the neural agents are likely shown relatively similar problems during training as at test time, including potentially stronger versions of the same theorems. There is also no comparison against non-neural approaches, such as Z3, Vampire, or similar theorem provers. 
To accept this paper, I would like to see stronger evidence that the introduced method produces significant improvements in prover ability. For example, the same method could be applied to datasets such as HOList, Mizar, and CoqGym which have received more attention recently than MetaMath.
Some additional questions and comments:
1. How big does the theorem graph G get? Since the relevance policy is over all nodes of the graph, this could lead to a very large neural network that would be difficult to fit into memory. Certainly not all 1M synthetic theorems could be generated in one graph.
2. The paper claims that all theorems from set.mm are used as background theorems in algorithm 1, including the test ones -- this potentially sounds like training on the test set, or even worse, having access to the test theorems as "proven background knowledge" at test time.
3. Please include some more details about the training of the Holophrasm baseline. Does it simply do RL on the human theorems, or does it also do IL on human proofs?