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".

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".