Is it possible to prove everything in mathematics by theorem provers such as Coq?

One of the computability results is that there must exist provable theorems in number theory that require very long proofs relative to their statements.

If $n$ is the encoding of a statement in number theory which can be proven, and $f(n)$ is the length of the shortest proof of that statement, then the function $$G(n)=\max \{f(k): k\leq n, k \text{ encodes a provable theorem}\}$$ is not only not computable, but it cannot be bounded above by any computable function, or else we could write a program that could essentially "find" all decidable statements - the set of decidable theorems would be recusrive, not just recursively enumerable. (I initially had an argument here about why that would be a problem, but that argument was flawed. I'm still pretty sure it is wrong for the decidables to be recursive, but it will take more work.)

In particular, then, for any total computable function $h$, there must be a provable theorem encoded by some $n$ such that the shortest proof, when encoded, is greater than $h(n)$.

So, in a practical sense, there will always be harder theorems, where we need more storage and compute time to verify the entire proof.

It is reasonable to believe that everything that has been (or can be) formally proved can bew proved in such an explicitly formal way that a "stupid" proof verification system can give its thumbs up. In fact, while typical everyday proofs may have some informal handwaving parts in them, these should always be able to be formalized in a so "obvious" manner that one does not bother, in fact that one is totally convinced that formalizing is in principle possible; otherwise one won't call it a proof at all. In fact, I sometimes have the habit to guide people (e.g. if they keep objecting to Cantor's diagonal argument) to the corresponding page at the Proof Explorer and ask them to point out which particular step they object to.

For some theorems and proofs this approach may help you get rid of any doubts casting a shadow on the proof: Isn't there possibly some sub-sub-case on page 523 that was left out? But then again: Have you checked the validity of the code of your theorem verifier? Is even the hardware bug-free? (Remember the Pentium bug?) Would you believe a proof that $10000\cdot10000=100000000$ that consists of putting millions of pebbles into $10000$ rows and columns and counting them more than computing the same result by a long multiplication?