> 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.