Agreed. But also formalising the statement of a theorem, or rather understanding the formalisation that the LLM suggested to you, is often a lot easier than understand the whole proof, especially if it's a formal proof.