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

I hope there's no hard feelings, by the way -- I wasn't meaning to be nasty to you in that comment. I guess I thought your reading was a bit uncharitable, but I understand that misunderstandings happen (very much including on my end) and I didn't mean to make a big thing of it, so I'm sorry if I came across rudely.