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.

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.  
