Comment by auggierose

No. What the paper says is that in principle, translating NL statements to Lean statements is hard. Nobody doubts that, translating informal to formal text cannot be formally proven correct, so...

Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.