Now that *AlphaGo* [has just beaten][1] Lee Sedol in Go and *Deep Blue* [has beaten][2] 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][3], [Mizar][4], [AFP][5]) 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*][6] 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][7] for "practice runs".

  [1]: https://en.wikipedia.org/wiki/AlphaGo_versus_Lee_Sedol
  [2]: https://en.wikipedia.org/wiki/Deep_Blue_versus_Garry_Kasparov
  [3]: http://us.metamath.org/
  [4]: http://mizar.org/
  [5]: http://afp.sourceforge.net/
  [6]: https://mathoverflow.net/questions/210888/what-technical-and-or-theoretical-challenges-are-involved-in-automatically-extra
  [7]: https://en.wikipedia.org/wiki/Reinforcement_learning