That's a good point. The formalizer was used to created the training data for the proof solver, so they likely worked on it more than if they just used it as a preprocessing step during inference. It is still possible that they worked on the formalizer until they got good results from it enough to create good training data, and then began training as soon as possible and did not spend too much time trying to improve the formalizer. Depending on how long the training was expected to take, perhaps that is a reasonable assumption. Although I think I agree more with your view now.