[kvakil]

From the article: "As an extra bonus, the generated proofs tend to be shorter than the ground truth proofs collected in CoqGym."

This feels a little misleading, the paper itself says that the phenomena "... suggests that theorems with longer proofs are much more challenging for the model." It'd be more interesting to see how the automated theorem proving length compares to the manual length for the same proofs (although I'd expect this to be biased downwards, for the same reason).