Because it is really hard to read and the level of detail is so high that even lemmas that you can read may have such enormous levels of detail that makes real understanding difficult given that humans have limited working memory.

Why not always write machine code? Why use programming languages at all?

Lean is a write only programming language.

Same reason humans write code not only for a compiler to translate into machine code but also so other humans can understand what we write, learn from it, modify it etc...

Because people need to understand what is being proven.

The example in Figure 1 should help understand why... the NL version is much more approachable for humans.