I don't see what the issue is. Isn't the entire point of LLMs that we can easily translate between languages? What better way to cross check the correctness of a proof than to run it on several different systems simultaneously.