Given that it was formalized correctly, which is far from trivial in many cases

(Of course LLMs can help there, get it right etc, just a caveat that people have to keep in mind)

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.