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.