It is the life's work of many people to make this question obsolete. More precisely, we aim to make mathematical assistants which are both pervasive and easy-to-use so that, in say 50 year's time, all high-quality journals would immediately reject a paper which has not been checked by one of these systems. [There are sub-fields of computer science where the time horizon for this seems closer to 5 years, with the 'best' papers already being machine-checked today].
Note that some people mis-interpret such statements. In the past, it is true that formal verification was extremely difficult and it intruded too much into the actual results and their write-up. But this has changed tremendously of late, where 'modern' verified papers (through the liberal use of literate programming tools and ideas) look the same as non-verified papers, they just come with attachments which contain the fully formal parts. Mathematical papers can then retain their human-oriented aspects of communicating the crucial ideas and insights, while allowing a certain lightening of the formalism in the text.
This is coming. Current mid-career mathematicians don't have to worry about this too much, but I would certainly advise the younger generation to keep an eye on these developments.
