>> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
As far as I understand the comment "the statement of the theorem" is the declaration of the theorem to be proved, not its proof. That it "usually covers a very small surface of the Lean code" also implies that the OP was only referring to the theorem, the thing to be proved, and not the proof that can run into many thousands of lines.
If I misunderstood then I don't think that's a problem? I don't believe my comment above comes across as rude or an attack on the OP? I think it's normal for this site for users to correct one another without it being a cause for bad feelings.