 Albeit not at the rate originally anticipated, automated reasoning is finding applications in mathematics. Of these, formal verification of proofs is of special significance since it not only provides a viable mechanism to check proofs that humans alone could not but it also has, as a side effect, the potential to redefine what it would take for a proof to be accepted as such. As the use of automated reasoning assistants becomes more widespread one can envision their use following a certain methodical order: First, automated reasoning tools are used for theory exploration and discovery. Then, having identified some target problem, the practitioner works interactively with an automated assistant to find proofs and establish facts. Finally, an automated proof checker is used to check the correctness of all final proofs prior to being submitted for publication and being made available to the rest of the mathematical community via the creation of new entries in a repository of formalized mathematics. It is indeed a matter of time before the application of automated proof assistants becomes an everyday affair in the life of the mathematician; it is the grand challenge of the automated reasoning community to make it happen sooner than later.