51
$\begingroup$

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

$\endgroup$
  • 5
    $\begingroup$ I don't understand the question if you are willing to make so strong assumptions regarding the issues related to computational complexity. Humans are bound to work with recursively enumerable sets of axioms, unless you somehow disprove the Church-Turing thesis. The set of theorems that can be proven from an r.e. axiom set is r.e and hence a computer is capable of proving any theorem that humans can prove, if it is provided sufficient resources. $\endgroup$ – Burak Mar 13 '16 at 0:23
  • 17
    $\begingroup$ I strongly disagree with the statement "We know that automated theorem proving is in general impossible." While it is true that efficient (e.g. polynomial-time) theorem-proving is impossible, that's not nearly the same thing. $\endgroup$ – Noah Schweber Mar 13 '16 at 0:30
  • 10
    $\begingroup$ "a machine learning algorithm trained on a large database of formal proofs" is not comparable to, say, training an algorithm to learn word-adjacency frequencies (which is well-achieved today). A proof has intricate logical internal structure, made explicit, e.g., by Georges Gonthier's computer proof of the $4$-color theorem. It is not clear that any machine-learning techniques could approach this logical complexity. $\endgroup$ – Joseph O'Rourke Mar 13 '16 at 0:48
  • 10
    $\begingroup$ Natural language processing today can involve far more than the digraph frequencies. It is possible to train a generative model that produces text one letter at a time, yet which closes quotes and understands that it might be in the middle of producing a bibliographical reference. It does seem a huge step to go from playing games, where the problem is primarily to estimate the strength of a position (approximate a function from a space of inputs to $[0,1]$) to writing a coherent proof, but it would be easier in some areas of mathematics than others. Undegraduate real analysis might be easy. $\endgroup$ – Douglas Zare Mar 13 '16 at 5:39
  • 5
    $\begingroup$ In case somebody want to discuss about the on-topicness of the question, there is a meta thread $\endgroup$ – user9072 Mar 13 '16 at 17:34

12 Answers 12

46
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Do you mean something like "technological singularity"? en.wikipedia.org/wiki/Technological_singularity $\endgroup$ – joro Mar 13 '16 at 9:13
  • 2
    $\begingroup$ I guess so, but it's nothing to do with exponential growth. There is absolutely no reason why mathematics is the sole domain of human brains, so over the long term it won't be. I'm assuming we won't kill ourselves with a virus that was "impossible" to create or do some other "impossible" thing that halts technological progress forever. $\endgroup$ – Brendan McKay Mar 13 '16 at 9:28
  • $\begingroup$ Even if computers become better at solving mathematical problems, there are some questions that will always be left unanswered (perhaps not mathematical ones). $\endgroup$ – Alan Mar 13 '16 at 18:06
  • 11
    $\begingroup$ Any guesses on when there will be a serious contender called "AlphaMath" or something for the International Math Olympiad? I'll put in 2030. $\endgroup$ – Dominic van der Zypen Mar 15 '16 at 15:29
  • 5
    $\begingroup$ @Dominic: It's really impossible to know. The type of well-structured self-contained problems that appear in the IMO are an easier target than mathematics-in-the-wild though. $\endgroup$ – Brendan McKay Mar 15 '16 at 22:19
30
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Is there similar progress in artificial intelligence? AFAICT computers are getting better on the Turing test, but this may be due to just heuristics. $\endgroup$ – joro Mar 16 '16 at 7:04
  • 1
    $\begingroup$ I'm not sure. Some of the publicized progress on Turing tests comes from people having lower standards for conversation now. There was a program that fooled a large minority of judges by claiming to be a kid speaking a second language, and most of what it said was strange and incoherent and didn't address the questions asked. That doesn't represent our progress toward strong AI. $\endgroup$ – Douglas Zare Mar 16 '16 at 18:28
  • $\begingroup$ By the way, it's not just a database of completed proofs that would help, but a collection of partially completed proofs, perhaps with an indication of whether they were successfully finished or not. $\endgroup$ – Douglas Zare Apr 2 '16 at 8:09
  • $\begingroup$ I think large database of formal proofs (say the size of arxiv.org) might find new results via series of implications among papers of which the authors weren't aware. Such database will find many contradictions too, due to errors in papers IMHO. graphclasses.org is probably one of the first steps in such formalization. $\endgroup$ – joro Apr 2 '16 at 8:16
18
$\begingroup$

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$"?

$\endgroup$
  • 1
    $\begingroup$ I like the last example. A key point in figuring out how to show that general quintics are unsolvable as opposed to quartics was to ask "what makes degrees 4 (or smaller) and 5 (or larger) fundamentally different?" and now we know that the answer is solvability of symmetric groups of corresponding size. I don't see how a computer would by itself figure out a correct question and a correct answer. $\endgroup$ – Wojowu Mar 13 '16 at 10:22
  • 28
    $\begingroup$ There are already computer programs that conjecture generalisations to observed facts. They aren't very good yet, but 100 years ago few people could imagine a computer at all. $\endgroup$ – Brendan McKay Mar 13 '16 at 11:04
  • 16
    $\begingroup$ Is it provable that computers can't ask math questions? Strongly doubt it. $\endgroup$ – joro Mar 13 '16 at 11:32
  • 2
    $\begingroup$ @BrendanMcKay I mentioned at the beggining "we ask questions" not "make conjectures" $\endgroup$ – Konstantinos Gaitanas Mar 16 '16 at 10:25
  • 2
    $\begingroup$ I don't see the difference. We ask a question, then we conjecture an answer, then we look for a proof or disproof. No reason a computer can't do all of that. $\endgroup$ – Brendan McKay Mar 16 '16 at 10:39
10
$\begingroup$

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.

$\endgroup$
  • 12
    $\begingroup$ To paraphrase your answer, our advantage is that we can enjoy doing mathematics while computers can't. $\endgroup$ – Māris Ozols Mar 13 '16 at 12:44
  • 2
    $\begingroup$ In the long term, there could exist a suitable notion of enjoyment for computers as well.. $\endgroup$ – dbluesk Mar 13 '16 at 13:32
  • 6
    $\begingroup$ I love mathematics as much as anyone but I don't think the analogy holds. Both chess and football are games we play/watch for entertainment. Yes, we could still do mathematics for entertainment but I think it would be pretty depressing since computers would know more than us. In this hypothetical world, there would be no point in looking for proofs or solutions to problems because the computers would most likely have already found multiple proofs for our problem and it's generalisations. $\endgroup$ – user230452 Mar 13 '16 at 13:54
  • 5
    $\begingroup$ Sure, mathematics will still be an enjoyable recreation for humans. But if you needed the solution of an actual difficult mathematical problem, you wouldn't take it to an amateur, you'd go to an expert, which in this case would be a computer. $\endgroup$ – Robert Israel Mar 15 '16 at 20:23
  • 4
    $\begingroup$ Jordan Ellenberg, in How not to be wrong, briefly speculates that whatever computers can do in the future will come to be regarded as "computation" and we will do "other math." $\endgroup$ – Kimball Mar 18 '16 at 0:02
7
$\begingroup$

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.

$\endgroup$
  • 9
    $\begingroup$ I disagree with the comment 'Beating a human at go is the same kind of work that had been done on chess'. There is a fundamental difference since the latest advance has been made by a pattern-discovering neural network based framework, which is precisely what gives it the creativity that chess playing computers lacked. We haven't discovered the 'Go' analogue of the grandmaster-defeating Chess algorithms, rather we now have a computer program which discovers those algorithms automatically if fed enough data from 'Go' games. $\endgroup$ – Piyush Grover Mar 13 '16 at 13:53
  • 7
    $\begingroup$ This is an interesting answer, but it is not clear that computers will be weaker "on creativity." $\endgroup$ – Gil Kalai Mar 15 '16 at 14:41
  • $\begingroup$ @Gil Kalai Thank you. Do you know some mathematical notions that capture the notion of creativity? It's a genuine question, if it exists it should be interesting to read about it. $\endgroup$ – logicute Mar 15 '16 at 14:58
  • 1
    $\begingroup$ @Piyush Grover Self-rewriting programs are nothing new, even if the techniques have clearly vastly improved. Weizenbaum argued that the fact that you don't understand the whole of the algorithm doesn't make it "intelligent" (Chinese room again). The fact that neural networks can be fooled by meaningless images (arxiv.org/abs/1412.1897) while pigeons can learn human aesthetic criteria show that there is a fundamental difference between human intelligence and good algorithms. $\endgroup$ – logicute Mar 15 '16 at 15:13
  • 1
    $\begingroup$ I don't know if you can infer a "fundamental difference" from the fact that this generation of neural networks can be fooled. People can also be fooled (although maybe not in the same ways). We just don't know as much about people's wiring. $\endgroup$ – Robert Israel Mar 15 '16 at 20:31
7
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Well on the other hand - don't you agree that the essence of the mathematical content (for example its truth or falsity) is independent of those judgements and cannot be in any way influenced by them? $\endgroup$ – მამუკა ჯიბლაძე Mar 15 '16 at 22:32
  • 5
    $\begingroup$ I think it would be much easier to train a neural net to estimate the average opinion of how beautiful a mathematical result is than to teach one to come up with interesting proofs. $\endgroup$ – Douglas Zare Mar 16 '16 at 0:24
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I wonder whether computers will be able to do "meaningful mathematics" much sooner than you suggest, but will only be able to work or communicate with the aid of a mathematician translator. I can envision a program given a set of definitions and taught to find interesting results much more easily than I can envision a program capable of reading and writing mathematical papers or strategically choosing broad research programs. $\endgroup$ – Neal Aug 3 '17 at 16:35
  • 1
    $\begingroup$ Similarly, I would guess that most students are able to work in a limited setting and attain (moderately) interesting results much before they have a broad understanding of their field, are able to define interesting research programs, and can envision results, techniques, and directions of interest to the community. $\endgroup$ – Neal Aug 3 '17 at 16:39
2
$\begingroup$

You might be interested in the recent following great peace from Quanta magazine 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.

$\endgroup$
  • $\begingroup$ The link is very interesting, but imo this "what to prove" does not make sense. Just look at the whole MO - you have questions you want to have answered. You do not choose these using inspiration or subjective aesthetic taste, they are blind spots left in the field you are exploring, you really need them answered to keep going. $\endgroup$ – მამუკა ჯიბლაძე Aug 3 '17 at 23:33
  • $\begingroup$ Well the original question started from chess and go. I somewhat agree with what you say - but only 99% there is still a 1% of belief that math is not just a mechanical proof of evident theorems. $\endgroup$ – Yochay Jerby Aug 4 '17 at 1:29
  • $\begingroup$ While it can grow into an interesting discussion on the question of "what is math" - since the question started from AI - let me give you an example that already exists in another field - music - check for instance J. S. Bach - Computer Generated Music - would it evolve to play Mozart? Jazz? Iggy pop and the stooges? $\endgroup$ – Yochay Jerby Aug 4 '17 at 1:39
  • $\begingroup$ It is hard for me to say anything about it, since I already know what it is and all kinds of subconscious associations intermingle. But in general, I could say about music the same I said about mathematics. Genuine music, by which I mean music designed to induce in the listener something definite that the composer aims at sharing with others, is created after the composer already has to share certain something which cannot be shared by any other means. Only after that (s)he begins to seek appropriate means to do it. So far, computers are in an entirely different situation, do you agree? $\endgroup$ – მამუკა ჯიბლაძე Aug 4 '17 at 5:27
-3
$\begingroup$

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]

$\endgroup$
-5
$\begingroup$

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.

$\endgroup$
  • 14
    $\begingroup$ And, yet, I write computer programs that deal (usually correctly) with 2 and even 3, every day. $\endgroup$ – Brendan McKay Mar 13 '16 at 9:02
  • 5
    $\begingroup$ @BrendanMcKay, very good point. You probably don't use Bourbaki's definition :-) $\endgroup$ – Mikhail Katz Mar 13 '16 at 9:02
  • $\begingroup$ Why is Bourbaki's definition of 1 not $\{\emptyset\}$? Surely von Neumann ordinals were around when Bourbaki was founded. $\endgroup$ – Burak Mar 13 '16 at 10:27
  • 4
    $\begingroup$ @Burak Link: dpmms.cam.ac.uk/~ardm/inefff.pdf $\endgroup$ – Todd Trimble Mar 13 '16 at 10:29
  • 2
    $\begingroup$ @ToddTrimble: Thanks. This was illuminating. It seems that Bourbaki is using the wrong definition (Remark 8.1). The correct $1$ only requires 217 symbols by Proposition 5.3. I must say that the most amusing part of the paper is the question "what will happen to a young innocent who decides to learn mathematics by reading Bourbaki, and to start with Volume I?" $\endgroup$ – Burak Mar 13 '16 at 11:00

Not the answer you're looking for? Browse other questions tagged or ask your own question.