[giraj]

Mechanized proofs ensure the correctness of the results they prove. That's useful. Indeed, the point of the article was that Voevodsky sought out proof assistants in order to ensure his math was correct.

As for your other questions: No, formal proofs are not intelligible to the average mathematician. They do not on their own grant insights, but the process of formalising a proof does often yield insights. (I speak from experience.) Not sure what you mean by "better"; they certainly don't replace ("informal") mathematical proofs.

[hgsgm]

Most mathematicians don't care if proofs are correct, only that they look correct to other mathematicians.

[giraj]

That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.