The mathematician and Fields medalist Vladimir Voevodsky on using automated proof assistants in mathematics:

[Following the discovery of some errors in his earlier work:] I think it was at this moment that I largely stopped doing what is called “curiosity driven research” and started to think seriously about the future.

[...]

A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.

[...]

It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.

[...]

Among mathematicians computer proof verification was almost a forbidden subject. A conversation started about the need for computer proof assistants would invariably drift to the Goedel Incompleteness Theorem (which has nothing to do with the actual problem) or to one or two cases of verification of already existing proofs, which were used only to demonstrate how impractical the whole idea was.

[...]

I now do my mathematics with a proof assistant and do not have to worry all the time about mistakes in my arguments or about how to convince others that my arguments are correct.

From a March 26, 2014 talk. Slides available here.