The title appears to derive from the single sentence "Our best model automatically proves 48% of the theorems in the validation set."
The actual work looks to be about converting existing proofs to a formalised graph based encoding (using ml)
In 10 years I think every mathematician will use formal methods, it will be like typing your proofs with a type writer not to. Moreover the problems are very amenable to smart tools assisting in the work, there is a smooth path from where we are now to a fully ai mathematician.
“In the experiments presented in this paper, we predict tactics and their arguments by looking only at the conclusion of the current sub-goal and ignoring any local assumptions that could be crucial to the proof. This is a serious limitation for our system, and in future work we would like to include the local assumptions list when generating the embedding of the goal.”