Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove. Otherwise, what happens if the LLM includes an underhanded addition to the lean code which leads it to output a false positive?

> Surely some understanding of the lean proof is required, to make sure it proves what it claims to prove.

Yes:

> The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say)

However, it is much easier to manually check whether the statement of the conjecture was formalized correctly than to manually check the whole proof.