[oh_my_goodness]

>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.

[fsmv]

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