No idea why you're picking on the author's minor grammar mistakes. They may not even be a native speaker. The article is perfectly understandable, I read it myself and didn't even notice the errors before you pointed them out.
> “ Of course, mathematicians gain a lot by doing this1, machine checked proofs reduce..”
This sentence is grammatical, the 1 is just a footnote (which you can click) - this could be improved typographically, I suppose. The rest are just minor mistakes - "are promising to", "with the Lean Theorem prover", "to non-mathematicians".
