>That's what's covered by the "assuming you have formalized the statement correctly" parenthetical.

Sure. But it's fair to ask how to validate that assumption.

Skilled humans must understand the problem and write the theorem statement.