No expertise at all on interactive theorem provers like Lean but I am familiar with Resolution-based automated theorem proving. In that setting, one writes down

No expertise at all on interactive theorem provers like Lean but I am familiar with Resolution-based automated theorem proving. In that setting, one writes down a theory, in the form of a set of first-order definite program clauses, and then presents a statement to the prover, then the prover proceeds to prove the statement is a theorem derived from the theory. Is that (other than the language not being definite logic) more or less what Lean does also? In that case, isn't all the work in writing down the theory, and isn't that the step where mistakes can creep in? Is that more or less what you're pointing out? That FLT is simple enough to state but the theory from which it is to be derived can be mangled and so accept FLT on the wrong grounds?