Now that AlphaGo has just beaten Lee Sedol in Go and Deep Blue has beaten Garry Kasparov in chess in 1997, I wonder what advantage humans have over computers in mathematics?
More specifically, are there any fundamental reasons why a machine learning algorithm trained on a large database of formal proofs couldn't reach a level of skill that is comparable to humans?
What this question is not about
We know that automated theorem proving is in general impossible (finding proofs is semi-decidable). However, humans are still reasonably good at this task. I'm not asking for a general procedure for finding proofs but merely for an algorithm that could mimic human capability at this task.
Another caveat is that most written mathematics at the moment is in a form that is not comprehensible to computers. There do exist databases of formal proofs (such as Metamath, Mizar, AFP) and, even though they are quite small at the moment, it is conceivable that in future we could have a reasonably sized database. I'm not asking whether you believe that a substantial amount of mathematics will be formalized one day — I'm willing to make this assumption.
Finally, there is the issue of the sheer machine power required to run this. Again, I'm willing to assume that we have a large enough computer to train an AlphaGo-style algorithm and then use reinforcement learning for "practice runs".
Best Answer
The day will come when not only will computers be doing good mathematics, but they will be doing mathematics beyond the ability of (non-enhanced) humans to understand. Denying it is understandable, but ultimately as short-sighted as it was to deny computers could ever win at Go.
This is not as depressing as it might sound, as we humans don't need to be left behind. Direct brain-computer interfaces will come too, and even the distinction between them will become blurred.
COMMENT: We were amazed when someone built a machine that could travel faster than a horse, then amazed when a machine let us fly into the air, and even go to the moon, then amazed again that millions of us could carry a tiny machine that identifies our position on the planet within meters and lets us talk instantly to anyone else on the planet, and amazed again that someone invented a machine that can edit life forms to make new life forms. But the very idea that a machine could do mathematics, that one is surely impossible! (By the way, I love the down-votes.)