Computing will continue to aid mathematical discovery, proving (useful) theorems like Four Color, or even formulating their own (useful) theorems before proving them.
For example, in Einstein's Special Theory, there's not a lot of deep mathematics (relative to the General Theory) so it's not too difficult to imagine Watson taking the problem and axiomatizing (just to see what would happen) that light speed is always constant (which is the key to everything else that followed).
But what about Descarte's insight that geometry could be described by algebra using a coordinate system, giving birth to analytic geometry? Or proving that it can't prove all true statements in arithmetic (Godel)? Or even asking the question?
I think we're a long way off from doing something like that in a machine.
Indeed, mathematics requires a big deal of creativity. You could argue it is a somewhat subjective discipline, as interesting questions receive infinitely much more attention than a random question. And how do you define what is interesting?
There are an infinity of directions you can take -- which for humans is fine, because they know that you eventually have to end up with something your peers find interesting as well. How would a machine do this? I feel this could be akin to train a computer to enjoy music.
While computers will continue to become more and more involved in theorem proving, it's not clear to me that they will be able to ask interesting questions within the next few years.
On the other hand, journal papers keep pouring every day at rates that are impossible to keep up. In the future this situation will be hopeless in the absence of some AI to guide us among that mess. But then again, papers are written in a combination of natural language and mathematics.
> Descarte's insight that geometry could be described by algebra using a coordinate system...
This was a new model which made a large class of insights more tractable to human minds. A theorem-finding computer probably wouldn't come up with the same kind of model(unless we specifically programmed it to), it would come up with models which made further insights more tractable to theorem-finding computers. Already, today, a huge part of the problem with creative computers is interpreting their results for humans.
For example, in Einstein's Special Theory, there's not a lot of deep mathematics (relative to the General Theory) so it's not too difficult to imagine Watson taking the problem and axiomatizing (just to see what would happen) that light speed is always constant (which is the key to everything else that followed).
But what about Descarte's insight that geometry could be described by algebra using a coordinate system, giving birth to analytic geometry? Or proving that it can't prove all true statements in arithmetic (Godel)? Or even asking the question?
I think we're a long way off from doing something like that in a machine.