What advantage humans have over computers in mathematics? 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".
 A: It boils down to creativity. What we truly admire in mathematical achievements are the creative leaps when creating new theories (category theory, calculus), not mathematical prowess, which is a tool. Good problem solving is also highly regarded, but it's also admired for the creative ideas it takes while doing the proof. 
Computers are terrible at creativity, but insanely better than humans at raw computational power. We don't even have what can barely sounds like a mathematical model for creativity.
When people thought computers could not beat people at chess, it was because they assumed it was a task that required creativity, and could not be done with only raw computational power, fine-tuned heuristics, and good interpolation from known results (in most games, this move fails, so it's probably a bad move). It's basically the Chinese room Gedankenexperiment all over again: you don't need to understand Chinese to form valid Chinese sentences given that you have a good enough grasp of the syntactic game. 
Gowers said in a talk that at least 90% of a mathematican's work is routine, and could very well be automated. This is exactly the same thing, to make most proofs you apply some heuristics, a few classical theorems and techniques. There's no reason to think that this could not be fully automated for a wide range of problems, given enough time. 
Now for mathematics, if humans were working at the low-level of axiomatic set theory, then they would have been out-competed by computers long ago. But the fact is that humans (at least, some) can work in inconsistent high-level systems, and fix the problems as they arise because they have a good intuition of what should work (take set theory, lambda-calculus, etc). 
Beating a human at go is the same kind of work that had been done on chess, so the misunderstanding was just on the true nature of what 'being good at chess/go/X' means, and in particular what it means computationally. We're getting a better idea on these thanks to the advances in proof theory, but that doesn't help with the question of creativity. Note that most 'creative work' can also be reduced to a short set of generic techniques (blending two ideas, changing a parameter, etc), but it doesn't really help getting to the next scientific revolution.
To come back at the issue at hand, the problem is not only finding proofs in mathematics; if you were to run an excellent algorithm that would give you tons of theorems, you would be well-embarassed in finding which ones are useful, and which ones are very convoluted tautologies with little content. Computers can be much better than humans at some mathematical tasks (like we know from a while that they are orders of magnitude better at arithmetic than humans), they are already much better at specific theorem-proving tasks, and the number of such tasks will continue to grow. This doesn't address the creative advantage humans have.
A: Being a shameless platonist, for me the answer is obvious. We only need mathematics since it is the only way to be able to reach certain things transcending ourselves - just as music or poetry is the only way to be able to reach certain other things (or maybe other aspects of the same things). Computers certainly may enhance our ability to reach these things and maybe even at some point will serve as a direct communication medium with them, but I don't see any sense in which the computers could replace either one or other side of that communication.
After a while - highly pleased to see tense controversy around this: +7-5 :D
Still later - now it is +13-7, spectacular!
A: The advantage that humans will have over computers in mathematics is that humans will be the judges of the value of whatever mathematics is done.  That is, the judgment of what mathematics is worth doing - what is an interesting question, what has beauty - will be done by humans, and this will give humans an intrinsic advantage, because the way humans explore and do mathematics is closely bound up with their aesthetic and moral judgments. 
A: 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.)
A: You might be interested in the recent following great piece from Quanta magazine In Computers We Trust? touching exactly on that subject.
Just a side remark — there is a difference between "how to prove" and "what to prove" when it comes to theorems — to some extent one of the beauties in math — is that there is a certain amount of inspiration or at least subjective aesthetic taste on what makes for an "interesting" theorem. In chess or go — you have a clear objective of winning a game with a fixed set of laws — but in math the objective itself — that is which theorems are worth while proving — is a huge part of the mathematical creative process.
A: The particular techniques used to make progress on go do not seem to help much with mathematics. While we might figure out how to get computers to prove deep theorems requiring the introduction of new mathematical ideas later, most of the work has yet to be done. 
Neural networks are reasonably good at regression problems, and most games can be expressed as regression problems. This means coming up with a good encoding of the game situations as vectors (say, as elements of $[0,1]^n$ or $\{0,1\}^n$) and then finding an approximation of a function of those vectors to $[0,1]$. In a game, we predict things such as the probability of winning from that position using perfect play or randomized strong play.
As far as I know, we don't have a good way to encode a mathematical situation (say, a partially written proof) as a regression problem. We could use something like ASCII, or better an encoding of a formal mathematical language, but this naive representation is of a type that would be expected to perform poorly. Further, what value would we associate to such an encoding? The probability that a slightly randomized brilliant mathematician can complete a correct proof from there within the next few pages? It would be difficult to get the evaluations of situations for training data. 
If we could get a huge database of well-written formal proofs, this would help. This might let a deep neural network find its own internal encoding (using unsupervised pretraining). However, while we can generate a huge amount (billions) of reasonable game positions rapidly through self-play, it's not clear what the analogue of this could be for mathematical proofs. If you use lots of minor variations on a short proof of the Pythagorean Theorem, or proofs of trivial facts, you would not prepare the network to find a medium-length proof of Fermat's little theorem or the prime number theorem, much less a longer proof of something open.
There was a lot of warning before computers became strong chess players, and before they became strong go players. Computers made steady progress of roughly 100 Elo points per year in chess from 1976 through 1986, for example, and computers have been steadily climbing the ranks on internet go servers. So far, we haven't gotten any such warnings about doing mathematics in general. We can automate calculations, integration, and combinatorial telescoping but those don't generalize easily. Further, we do a lot more than prove things in mathematics. 
A: I believe this is a topic where it is better to steer clear of philosophy and be concrete.  The natural way to consider this problem is to simply compare mathematics to those areas where computers have already proved to be superior to humans, such as board games. 
It is difficult not to notice that mathematics is not a game. Theoretically, the task of proving (say) a conjecture can be formalized, and made into a sort of combinatorial problem. However, this is not how we humans do mathematics, and it is not how computers would do if they are supposed to have a chance at a problem like Poincare conjecture. 
The thing is, once you are above the purely formal level, the task of proving a conjecture (or, say, finding a new formula) becomes extremely complicated already as a task. You can learn the rules of chess in ten minutes, and after this you will be able to play, even against a grandmaster. (You won't be able to win, but this is a different story.)  In comparison, people learn for decades just to be able to read published papers. The ``rules of the game'' are many orders of magnitude more complex. 
It may be possible to teach  a  sufficiently advanced computer  these ``rules'', but this is not a piece of cake. The first step is formalization of all mathematics. (Maybe not necessarily formalization is the usual sense, but one way or the other we have to teach a computer how to  read modern mathematical literature.) This is already a formidable task, which won't be accomplished any time soon. But  at least, it seems withing reach.
After this, a computer will be in a position of a beginner who has just learned the rules. (By the way, the same may be said about a human graduate student.)
The second, and still more difficult task, will be to upgrade someone who can play to someone who can win. Probably not impossible, but much  more difficult then with Go (for plenty of reasons).
The point is, actual ``computer mathematicians'' is a matter of such a distant future that it does not make much sense to talk about it now. When (or if) such a time will come, everything will be different.
To answer the question itself, there are no  fundamental reasons why a machine  couldn't reach a level comparable to humans, when it comes to mathematics. But there are reasons why  this is extremely difficult to achieve in reality.  In particular, modern AI technologies, regardless of their success in many other areas, would likely be useless.  
A: I believe that our advantage is the following:   

The fact that we ask questions.

Remember that mathematical induction was invented/discovered because we wanted to answer the following question:
how can we prove $1+2+...+n=\frac{n(n+1)}{2}$ is valid for every $n\in \mathbb{N}$?
If we ask questions we are getting better.I doubt that a computer would invent/discover group theory in order to investigate the unsolvability of algebraic equations because there would be no question like   

COMPUTER:
  "We can solve the $ax^2+bx+c=0$ but what about $ax^5+bx^4+cx^3+dx^2+ex+f=0$"?

A: 
What advantage humans have over computers in mathematics?

There is an active research in machine learning world, more specifically in NLP (natural language processing) that tries to answer contrary, and even more general question:

What computers can do, that we previously thought that only humans can do?

In my opinion the most interesting approach is an ongoing collaborative benchmark for NLP models called BIG-bench; it is just a bunch of tasks which you can test your model on, or test yourself (or your friends, family or foes)! What is important, you can also add your own tasks.
Regarding the OP question, you can browse the tasks by the keywords here. For example you can test if your model is capable to "understand" Mathematical Induction. You may ask it if the following is true:

1 is an odd integer. Adding 4 to any odd integer creates another odd integer. Therefore, 9 is an odd integer.

You can even "check" if you model is self-aware. Moreover, regarding @logicute answer, you can "measure" your models creativity in various of tasks.
So, can computers do math already or not?... It hasn't been tested carefully yet, but not yet perhaps. Will they?... To answer this question I believe we should keep track of the projects like BIG-bench.
A: I do not really know the answer, but I am inclined to agree with Brendan McKay's answer which I will just paraphrase as in the long term, none.
As a counterpoint though, I do not think this will mark the end of human mathematicians since I regard mathematics as a fundamentally human endeavor.  For example, even though computers have surpassed humans in chess playing ability, I still enjoy playing chess (against fellow humans) and watching chess (played between two humans).  For example, Anand's missed tactic against Carlsen in Game 6 of the 2014 World Chess Championship was very dramatic to watch live.  
As another example, one can imagine that eventually we will be able to design a team of robots that can beat any human football team.  This does not mean humans should stop playing or watching football. 
For me, mathematics is more than just knowing which mathematical claims are true or false.  There is a human community of mathematicians that one should actively engage in by presenting at conferences, writing papers/books that are humanly digestible, mentoring other humans, etc.  
A: There is no doubt that computer will HELP doing mathematics, and they are already helping. Computers are better in doing some jobs, humans are better in doing other jobs. I believe that there will always remain something in mathematics that only humans can do.
It is difficult to predict, of course what exactly computers will do better.
50 years ago it was widely believed that soon computers will translate text from one language to another, but playing chess well seemed more difficult for a computer. Now computers play chess better than humans, but their ability to translate is very limited.  Try to translate a moderately difficult text with any program or with Google translate, and you will obtain garbage in most cases.
A: Thomas Breuer has proven (Classical Observables, Measurement, and Quantum Mechanics, The Impossibility of Accurate State Self-Measurements) that an observer cannot predict the future of a system in which he is properly contained (even probabilistically). The proof is mathematical, by diagonalization. This includes the cases where the observer would use any possible tools or machines. Basically, the observer does not have a well-defined state as a starting condition for applying physical laws.
This means that the observer is not simulable on a Turing machine, while any real-world machine can be simulated by a Turing machine, and by any conscious observer.
This shows an asymmetry a robot cannot simulate the observer but the observer can simulate a robot, and this is a fundamental result.
One should note here that other people would be similar to robots in this respect (e.g., predictable).
So, there is only one human, who has principal advantage (not in performance!) over any existing or conceivable machine.
A: Human mathematical creativity is not reducible to computation.  An illustration of this is that human beings would have an easier time figuring out Bourbaki's Set theory.  As A. Mathias showed, Bourbaki's definition of "1" requires billions of characters.  The definition of "2" is probably inaccessible to modern computers.  The Bourbaki definition is certainly inefficient from the computational standpoint, but the point is that a (human) reader can follow the reasoning without being able to process a billion chips.
A: Added For me one advantage of humans is the experience in mathematics for thousands years, including teaching/collaborating.
On this scale, for me, computers are just "newborns".
Some of the older science fiction already came true.
Also, some predictions about computers were quite off.
http://www.rinkworks.com/said/predictions.shtml

"I think there is a world market for maybe five computers." -- Thomas Watson, chairman of IBM, 1943.
"Where a calculator on the ENIAC is equipped with 18,000 vacuum tubes and weighs 30 tons, computers in the future may have only 1,000 vacuum tubes and weigh only 1.5 tons." -- Popular Mechanics, 1949


McKay's answer appear close to Technological singularity

The technological singularity is a hypothetical event in which artificial general intelligence (constituting, for example, intelligent computers, computer networks, or robots) would be capable of recursive self-improvement (progressively redesigning itself), or of autonomously building ever smarter and more powerful machines than itself, up to the point of a runaway effect—an intelligence explosion[1][2]—that yields an intelligence surpassing all current human control or understanding. Because the capabilities of such a superintelligence may be impossible for a human to comprehend, the technological singularity is the point beyond which events may become unpredictable or even unfathomable to human intelligence.[3]

