The biggest problem in mathematics has never been proving theorems. Mathematics was never focused on proof until the formalization of math became popular approximately 100 years ago. Mathematics is used as a tool to explain the world and to create the least-complex model which predicts the data.
So computers can aid us in verifying our work--but ultimately we aren't interested in determining all the possible logical theorems. Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely.
It's a subtle difference, but for computers to solve that problem requires for them to have a certain understanding of humans and our goals with science.
So computers can aid us in verifying our work--but ultimately we aren't interested in determining all the possible logical theorems. Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely.
It's a subtle difference, but for computers to solve that problem requires for them to have a certain understanding of humans and our goals with science.
I think that's more than 10 years out.