Is it possible to prove everything in mathematics by theorem provers such as Coq? Coq has been used to provide formal proofs to the Four Colour theorem, the Feit–Thompson theorem, and I'm sure many more. I was wondering - is there anything that can't be proved in theorem provers such as Coq?
A little extra question is if everything can be proved, will the future of mathematics consistent of a massive database of these proofs that everyone else will build on top of? To my naive mind, this feels like a much more rigorous way to express mathematics.

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?
