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

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.