In the grand scheme of things all the errors he mentioned do not make a difference to the overall direction of the proof. Syntactic errors in programs on the other hand do. Unused variables, equality instead of assignment, declared but uninitialized variables, etc. are almost always bugs. That's not the case with math.
That's not to say this line of reasoning is not worthwhile. PLT Redex already does something similar for programming language semantics: http://redex.racket-lang.org/. Catching bugs in programming language semantics works for the same reason catching bugs in C works. There is a formal grammar with well-defined meaning that doesn't exist in general mathematical discourse. There is work being done in that direction as well: http://homotopytypetheory.org/book/. I wouldn't call that linting though.
> In the grand scheme of things all the errors he mentioned do not make a difference to the overall direction of the proof.
They make a huge difference if the reader wants to reuse a certain formula without deriving everything in sight. The time necessary to use a formula is no longer O(1), but O(n) with n being the length of the preceding discussion.
It also means you can't look at two expression and immediately check if they are equivalent as the variables might have different semantics.
Plus, you don't get to correct the mistake in the original, so every time you (or someone else) have to read it, you might need to redo the calculations just to be sure.
Then you and I are talking about different things. I don't read a mathematical proof to see what formulas I can copy. I read a mathematical proof to re-use the techniques in some other domain and to understand it I have to follow along and re-create bits and pieces of the proof. Obvious mistakes like the one mentioned in the post do not hinder that process. Less obvious errors would not be caught by a linter.
As for correcting mistakes I usually go to the author's homepage to find the most up to date versions along with errata. These days most papers are put up on the arxiv anyway which is often more up to date than whatever is printed in a journal so fixes for minor errors is again a non-issue.
I'm not talking about "reading a proof to see what I can copy", it's about being able to rely on what is written there. Also, there are many papers that serve as references that I want to be able to look up quickly. Rederiving every result any time I want to use it is not the way to go.
So... Kind of like the risk you take when you copy and paste code without first attempting to understanding it? I can't say that I've ever read through a proof just to nab a formula without even thinking through the material.
That's not to say this line of reasoning is not worthwhile. PLT Redex already does something similar for programming language semantics: http://redex.racket-lang.org/. Catching bugs in programming language semantics works for the same reason catching bugs in C works. There is a formal grammar with well-defined meaning that doesn't exist in general mathematical discourse. There is work being done in that direction as well: http://homotopytypetheory.org/book/. I wouldn't call that linting though.