No, the important part is that the proof is proving what you think it's proving, meaning you only care about the statement being proved (i.e. the signature/type of the proof term), not the proof itself. Generally the statement will be much smaller than the proof, so manually checking it (or manually writing it) is much more viable than checking/writing the proof.
> I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
Sure, that's why you have the check that the statement being proven is what you want it to be. Then any error in the proof _will_ be captured by the type checker.