It may be for this theorem there's a succinct description, but still needs to be checked carefully. However, there are others that are non-trivial.

In some cases you're right, but I think that's often a symptom of mathematics in Lean being relatively immature (i.e., it will get much easier with time). Even then, verifying the statement in Lean is correct is still much easier than verifying the natural language proof is correct.