A turn for what? Well, I have seen twice the same succession of events. Firstly, outstanding specialists of a domain assert, without any justification, that an AI system could never outsmart the best human experts of this domain. For many years, they are right, and they laugh at the poor results obtained by the first programs. Then, suddenly, everything changes: artificial systems outperform the best humans.
This happened for Chess, and recently for Go. I believe that the next domain where this sequence of events will occur is mathematics, a propitious domain for several reasons. Firstly, as games, mathematics is far removed from reality; the researcher has not to confront the many constraints coming from the real world, such as it is the case for driving a car. Secondly, games have been created by humans, based on what they can do best: from the start, we, humans, are in a good situation. On the contrary, mathematics has not been developed to solve problems that are not too difficult, but to solve useful problems. It is not obvious that mathematics is as well suited to our capacities as games; therefore, artificial beings are in a much better situation than for games: they could use all their qualities, in situations where they are essential, and where we are not very good. Our intelligence results from the importance for our ancestors of hunting and fighting for surviving and breeding. The fighting aspect is important in games, but not in mathematics. There is no reason why human intelligence would be well adapted to mathematics. It is simply the case that some capacities developed for other goals are somewhat helpful for mathematicians.
For the present time, no limit is known that would prevent AI systems to outperform human mathematicians. The well-known incompleteness theorems restrict what can do any cognitive system, human or artificial. Nobody could ever prove a result if no proof exists for this theorem in this theory.
Fist-class mathematicians have claimed that machines could never be very strong in mathematics, but they never justify this assertion. For them, it is not necessary, it is evident. However, a good mathematician should know that, when there is a mistake in a proof, it is often when one says that something is evident. Probably, they are so confident because they do not see how this could be made. This is normal: they are mathematicians, not AI researchers, this is not their job. In the same way, Chess and Go players’ job was not to write Chess and Go programs: they could not foresee what happened.
Mathematics is also a very interesting domain for AI because their results are extremely helpful. It is natural to invest in artificial mathematicians: their discoveries will be more useful than those of a Chess program. Naturally, their role will not be only to prove conjectures: they will have to build new mathematical theories. Pioneering works, such as those of Douglas Lenat, have shown that an artificial mathematician could discover concepts it did not know. For instance, for a function, it is interesting to consider the situations where the values of two arguments are the same: from addition one discovers the concept of double, and from multiplication, the concept of square. As extreme situations are often remarkable, considering them leads to the concept of number with few divisors, the prime numbers. Surprising its author, Lenat’s program studied also the numbers with many divisors; then Lenat discovered that Ramanujan had already studied them. Naturally, a lot of work is necessary for developing systems with many more possibilities that this old system, but this is certainly not impossible.
CAIA has a powerful method for solving problems where it cannot use a combinatorial method because there are too many possibilities, and even sometimes an infinite number. With the meta-combinatorial search, one does not consider all the possible values of a variable, or all the legal moves; instead, one considers many methods for trying to solve the problem. One can waste a lot of time, with methods that fail; however, at the end, one has an excellent solution, as one keeps only the methods that are necessary for justifying it. When one has a good set of methods, one may find sometime surprisingly elegant solutions. As computers are much faster than human brain, they can perform a meta-combinatorial search wider than those made by human mathematicians.
To date, AI has progressed rather slowly in the Universities, which are certainly not the right place for developing very complex systems quickly. Since recently, industrial firms have heavily invested in AI realizations; it is no coincidence that IBM succeeded for Chess and Jeopardy!, and Google for Go. They moved to the upper category very fast: before AlphaGo, I did not think that an AI system would win again one of the best professional Go player before ten years.
In view of the importance of mathematics, it will be tempting to create a competent team, with substantial resources: they could rapidly have results more valuable than would be expected. Human mathematicians would help us to understand the results of their artificial colleagues, so that they could be used efficiently and effectively. Naturally, they will also continue to do mathematics for the fun, in the same way as Chess and Go players are always playing their favorite game.
Since correct programs or algorithms are proofs (and vice versa, a proof is equivalent to an algorithm), algorithmics & program synthesis is also a domain where an AI system could excel.
And the advantage for an AI system to focus on computer science is that the created algorithms could be useful for the AI system itself. In other words, the most useful mathematics for an AI system (running on some computer) is computer science…
BTW, an interesting issue is to show sketches of proofs which are intelligible to humans (also not all of them are; obviously, an AI system could create proofs which are made of many cases, far too much for any human to understand).
Since notation matters in math (to make it intelligible, as every marth tea)Showing intelligible proofs has also as a small sub-problem the elegant typography of the proof; concretely, it would be nice if CAIA could output proofs e.g. in LaTeX or MathML (two de facto standards for representing equations)
j’ai tapĂ© trop vite, faudrait remplacer le dernier paragraphe par (previous last paragraph should be replaced by):
Since notation matters in math (to make it intelligible, as every math teacher knows and requires from students), showing intelligible proofs has also as a small sub-problem: the elegant typography of the proof; concretely, it would be nice if CAIA could output proofs e.g. in LaTeX or MathML (two de facto standards for representing equations).
Notice also that math typography is a very difficult thing: Both Knuth & Lamport (two outstanding computer scientists) dedicated years of their life to that very interesting problem. Knuth invented TeX and Metafont and Lamport designed LaTeX above TeX.