The OpenAI proofs were all in English, and discovered by reasoning in English. Only afterwards was a portion of them translated into Lean. This step was only done to convince the mathematicians that the proofs were correct.