[IsTom]

Human-written proofs are not written in Lean to be checked easily and there'll be potentially many formalizations for written prose and only some of them will be what the author intended. You need to pick the right formalization before you can say that this proof has local errors.

[lblume]

If a human reviewer rejects a proof, what do they consider apart from local errors? Formal proofs have formal local errors (which can be checked mechanically), while informal proofs have informal local errors (which require humans and some degree of hermeneutics to check). Am I missing something?

[IsTom]

It might be using some nonlocal context e.g. something similar was proved earlier in the proof and the reader is assumed to remember and/or generalize this or there's some assumptions that are stated only in the beginning. There's also probably a bit of skipped proofs of the kind "I'll be able to do this if pressed, but so will the reviewer".