We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses on generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the-art RL approaches that were previously not applied in theorem proving. In particular, we show that curriculum learning significantly outperforms previous learning-based proof guidance on a synthetic dataset of increasingly difficult arithmetic problems.
In the paper, the authors present a new algorithm for training neural networks used in an automated theorem prover using theorems with or without proofs as training data. The algorithm casts this training task as a reinforcement learning problem, and employs curriculum learning and the Proximal Policy Optimization algorithm to find appropriate neural network parameters, in particular, those that make the prover good at finding long proofs. The authors also propose a new dataset for theorems and proofs for a simple equational theory of arithmetic, which is again suitable for improving (via learning) and testing the ability of the prover for finding long proofs. The proposed prover is tested against existing theorem provers, and for the authors' dataset, it outperforms those provers.
I found it difficult to make up my mind on this paper. On the one hand, the paper tackles an interesting problem of improving an automated theorem prover via learning, in particular, its ability for finding long nontrivial proofs. Also, I liked a qualitative analysis of the failure of the curriculum learning for tackling hard tasks in the paper. On the other hand, I couldn't quite make me excited with the dataset used to test the prover in the paper. The dataset seems to consist of easy variable-free equational formulas about arithmetic that can be proved by evaluation. Of course, I may be completely wrong about the value of the dataset. Also, if the dataset includes variables and other propositional logic formulas, such as disjunction, negation and conjunction, so that the prover can be applied to any formulas from Peano arithmetic via Skolemization, I would be much more supportive for the paper. Another thing that demotivated me is that I couldn't find the discussion about the subtleties in using curriculum learning and PPO for the theorem-proving task in the paper. What are the possible design choices? Why does the authors' choice work better than others? 
I added a few minor comments below.
* abstract, p1: "significantly outperforms previous learning-based". When I read the experimental result section, I couldn't quite get this sense of huge improvement of the proposed approach over the existing provers. Specifically, from Table 4, I can see FLoP performs better than rlCoP, but I wasn't sure that the improvement was that significant (especially because rlCoP might not have given a chance to be tuned to the type of questions used to train FLoP -- I may be wrong here). I suggest you to add some further explanation so that a reader can share your sentiment and excitement on the improvement brought by your technique.
* p2: The related work section is great. I learned a lot by reading it. Thanks.
* p4: I think that you used the latex citation command incorrectly in "learning Resnick ... Chen (2018)"
and "features Kaliszyk ... Kaliszyk et al. (2015a; 2018)".
* p6: discount factor) parameters related ===> discount factor), parameters related 
* p8: a a well ==> a well