The prover runs in iterations. In each iteration, it69 travels down from the root node.

Human Synthetic Generator Relevance Substitution T est proofs found proofs proofs T op-1 T op-5 T op-20 MRR Prob Accuracy (903 in total) 7125 0 - 43.27 69.57 We thank all reviewers for their thoughtful comments. Individual questions are addressed below. R1 -There is not that much novelty in the paper . We believe this is an important direction that worth more exploration in the AI/TP community.

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 human-written 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 improves the theorem prover and advances the state of the art of automated theorem proving in Metamath.