Why would they do that, knowing that the one known to be correct is the Lean one? Just to claim that the (correct) Lean proof did not translate well to English? That would be weak, and a colossal waste of energy and time.

Why do people program in Python instead of writing machine code?

Why are review papers published? Executive summaries? "Introduction to X" books?

People's time and computational resources are finite. Summarising information -- ideally in structured ways that preserve important properties, but even in informal, unstructured ways -- is critical for making any kind of progress in this world.