What areas of math can be tackled by artificial intelligence?

Artificial intelligence is nearing, with image/speech recognition, chess/go engines etc. My question is, what areas of math that are interesting to mathematicians, is likely to be the first to be able to be tackled by artificial intelligence? Is there some areas of math where some open conjectures or similar was solved by AI? Has AI been of use in math at all yet?

Most of the current successes in artificial intelligence are due to the rise of neural networks , "neural networks" work by training themselves to find structure in the data more efficiently.

"Image/speech recognition" are successfully solved by neural networks because their structure can be easily exploited ,

But mathematics is not like this , you cant create a database of lots of theorems and train a neural network on that to generate a new theorem.

Image/speech recognition is not an "intelligent" task , neural networks use 10 times or even more speech data than an average listens to attain this accuracy. But these are tasks which even a toddler could do with ease.

To tackle mathematics , we should first move towards creating a machine that has a "reasoning" ability , or in the language of AI "artificial general intelligence" . Current state of research in that direction is very low or even non-existent , so in near future we can't expect any breakthroughs in mathematics with AI.

One way of looking at this is , we have successfully developed functions that can classify and distinguish features of images , speech , or in general "patterns". But there is still lot of work to be done one machines that can make use of these functions to reason.

As mentioned in a comment by Lorenzo, there are some theorems where computers were involved in the generation of the proofs. Many of these involved brute-force, exhaustive search processes. Whether or not this counts as AI is debatable. I'd personally say exhaustive search is one of the simplest, most straightforward AI approaches.

Other than such approaches, the most closely related class of problems that researchers tried to address using AI is probably automated program synthesis: automatically generating simple programs based on desired input-output pairs. See, for example, this and this paper. As you would expect, these do not always work ideally and have only been successful so far (to the best of my knowledge) for relatively simple programs, but there is progress.

In principle, proving theorems seems like a rather well-defined problem for search techniques in AI to tackle. For example, if you view an Equation or a set of Equations that are known to be true as a "state", and all legal mathematical operations to manipulate one or more of those Equations as "actions", and a description of what kind of theorem you're trying to prove as a terminal state, you've got all the standard ingredients you need to define a search problem. Whatever search algorithm you like (e.g. Monte-Carlo Tree Search) should be applicable.

In practice, the size of the action space will likely be prohibitive (it's probably even difficult to fully enumerate and define the action space). It's certainly not going to be an easy search problem, but not inherently "impossible" either. I could see recent trends of combining Deep Learning with search algorithms like MCTS (e.g. AlphaGo) being useful here; there is plenty of training data in the form of existing, human-written proofs. These could absolutely be used to learn what kinds of steps humans tend to take when dealing with certain kinds of problems/equations, and provide some information for a search algorithm as to which parts of the search space would be plausible for a human mathematician to explore.

I don't think there are any areas of mathematics where such techniques would inherently be more likely to be applicable than others. It seems to me like the definition of the problem (formalization of state space, action space, etc.) would always be relatively similar, regardless of what area of mathematics we're talking about. I'm personally in AI first and foremost though, not a mathematician, so there may be something I'm missing here.

For combinatorial number theory with AI, see the dialogue between the mathematician and the computer as envisioned by Tim Gowers. (This was the perspective from 2000 on "Will Mathematics Exist in 2099?", section 2 of the ps or pdf.) Note that he says other areas of math would not be as easy, and that this would depend on "a mathematical database which is much more sophisticated than anything we have at present."

For special functions, see the Wolfram functions site, where such a database was up and running by the time Gowers's paper was published in 2004. So that area is also promising for Gowers-style AI.

There are two bottlenecks in the flowering of Mathematics:

The gap between intuitively 'knowing' a mathematical truth and rigorous proof.
The dissemination of rigorously proven mathematical truths to the world at large.

In both cases, opportunities for the application of AI aren't obvious.

Intuition and rigor (induction and deduction) aren't obvious bedfellows but both are needed for important mathematical advancements. According to Leonhard Euler, as quoted by Polya:

The properties of numbers have been mostly discovered by observation, and discovered long before their truth has been confirmed by rigid demonstrations. The kind of knowledge which is supported only by observations and is not yet proved must be carefully distinguished from the truth; it is gained by induction, as we usually say. Yet we have seen cases in which mere induction led to error.

Intuition isn't only the first step to proof. It generates the interesting ideas that capture the imagination and fuel both mathematics research and 'cranks'. This capturing of imagination is undoubtedly important: See Fermat's Last Theorem, Hilbert Problems, Guy's Unsolved Problems in Number Theory, The Clay Millennium Prize Problems, et.al. In fact, humans have the realm of intuition covered quite well. However, for every hyper-intuitive Ramanujan, there are many more intuitive would-be mathematicians whose ideas will die on the vine, or be wrong, or be published and never thought of again. The same will be true of populations of highly intuitive math-AIs. The missing ingredient is not induction but rather deduction.

Now if AIs achieve superhuman deduction, they could be assigned to attacking outstanding problems. This was the gist of Hilbert's 23 Problems, a list of the most important unproven conjectures in 1900. The second problem was essentially this: prove that Math isn't a house of cards, built on false premises. In 1931, Godel's Incompleteness Theorems gave an unsettling answer: we might never know. Godel showed that in any axiomatic system there are undecidable propositions (they cannot be proven true or false) and that given only the axioms of arithmetic, the consistency of arithmetic is undecidable. In other words, if you assign an open question to the best AI, there is no guarantee that a proof is even possible.

Not only is the gap from intuition to proof a potential dead-end, very few humans are willing and able to parse even their own intuitively generated ideas. Grigori Perelman can no longer be bothered to explain his Fields Medal winning proof. Shinichi Mochizuki claimed a proof of the abc-conjecture in 2012 and six years later it has yet to be dismissed or accepted. Maybe they both feel like an average professor, trying to explain mathematics to an eager amateur. Maybe Mochizuki is the crank and academia, with its norms of conferences and peer-reviewed journals, isn't capable of discerning the difference.

Despite the popular fascination with 'genius' as a synonym for inexplicable intuition, the opportunities in math research are actually the leaps from induction to deduction and again to dissemination. Although AI is progressing, (DeepMind's Alpha Zero is looking pretty good), AI is seemingly very far from contributing to mathematics.

Computers are pedants.

Pedantry and mastery are opposite attitudes toward rules. To apply a rule to the letter, rigidly, unquestioningly, in cases where it fits and in cases where it does not fit, is pedantry. … To apply a rule with natural ease, with judgment, noticing the cases where it fits, and without ever letting the words of the rule obscure the purpose of the action or the opportunities of the situation, is mastery. -Polya, How To Solve It

But humans are fallible.