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.
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 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?
If a programming language compiler isn't guaranteed to be re-producible, then yeah, you'd have to revert to machine code.
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...
Not only that, we also have code comments and standalone documentation.
A programming language, when compiled, is a guaranteed reproducible result. If you recompile a program, you get the same thing each time.
The point of the article is that natural language is not these things.
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.
If its ambiguous or wrong, then what are you understanding ?
Is not a natural language (NL) proof a demonstration of mastery and understanding?
If you understand the Lean, then you can create a NL proof. The LLM clearly doesn't understand the Lean code it produced.