Comment by fn-mote
5 hours ago
> the NL proof may be wrong. But who cares?
The people trying to understand the proof are probably following the natural language version. So they care.
I wouldn’t be surprised at all if that’s how this paper (which I did not read) arose.
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.