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".
“ developments, namely at the forefront of mechanised mathematics, is promising to..”
“ to formalise, real, novel and cutting-edge mathematical results the Lean Theorem prover.”
“ Of course, mathematicians gain a lot by doing this1, machine checked proofs reduce..”
“ there are additional benefits that this also provides non-mathematicians”