# Are computers going to be able to discover and prove important mathematics theorems? [closed]

Are computers going to be able to discover and prove important mathematics theorems within, say, 20 years?

-

## closed as not constructive by Asaf Karagila, Zhen Lin, Nate Eldredge, Qiaochu YuanApr 18 '12 at 5:39

As it currently stands, this question is not a good fit for our Q&A format. We expect answers to be supported by facts, references, or expertise, but this question will likely solicit debate, arguments, polling, or extended discussion. If you feel that this question can be improved and possibly reopened, visit the help center for guidance.If this question can be reworded to fit the rules in the help center, please edit the question.

'Important' is not a term well defined. and why 20 years ? what are you thinking about ? I suugest studying some computabilitytheory, it might give you some answers. –  Belgi Apr 17 '12 at 9:31
theorymine.co.uk –  pedja Apr 17 '12 at 9:41
computers don't think. the hard part is formulating the right definitions and questions and gauging the importance of derived consequences. these are creative acts. –  bgins Apr 17 '12 at 9:48
"Important" is not a well definded term, but the meaning of it is obvious. For example, Poincare conjecture(now theorem) is obviously important. Why 20 years? Because it's reasonably near future. 100 or 200 years are too far ahead and nobody here will be alive in that far future. So the question would be almost meaningless. –  Makoto Kato Apr 17 '12 at 10:02
Closed. This is a highly nontrivial question and far beyond the scope of math.SE. –  Qiaochu Yuan Apr 18 '12 at 5:40

Doron Zeilberger has put on his computer program, under the name of Shalosh B. Ekhad, as a coauthor on several papers. On MathSciNet, he is listed as having 23 publications. Here is his homepage. When it comes to things like the WZ method, the computer does most of the work in the proof. His program actually does discover and prove things, in a way. But, of course, he had to program it to know how to do that.

-

I think people are mixing up the difference between using a tool to assist in solving a problem, and having the tool solve the problem itself. There is a major difference between a Roomba and a Dyson vacuum. Building a Roomba is a much more difficult task and requires fairly advanced graph theory algorithms to do path finding as well as a notion of a 'goal'. To get a computer to really prove a theorem by itself I think we're going to need to set up a lot of things that don't exist yet. For one, we need to completely convert our mathematics to symbolic language, including concepts such as the real numbers which AFAIK no one has done yet. The computers would probably have to start from a set of axioms and slowly build out a 'graph' of theorems and implications. Useful theorems would be those with a high number of 'edges' on the graph. Basically, we need a better understanding of metamathematics and a better idea of what it is we're doing when we do mathematics before we can automate it. Before we taught computers to play chess our idea of the game was very intuitive. However, we realized that what humans have is a very large, highly pruned and optimized decision tree for which move to make. Once we're understood this it didn't take too long to teach a computer how to do it, and they are now the best chess players in the world. It's only a matter of time before computers become better than us at proving theorems, we just need to be able to articulate to them what it is they're supposed to be doing.

-
This is a nice answer, and certainly some people believe that computers will someday be able to construct fruitful definitions, prove interesting theorems, or even develop whole new fields of math. But I should point out that some will disagree on practical or philosophical grounds, and that the obstacles really are big. Even though computers can beat humans at chess, they are very far from playing chess like a human does-- people are still vastly better at identifying the few good moves to consider each turn, while a program exerts a lot of computation to eliminate "obviously" bad moves. –  Jonas Kibelbek Apr 17 '12 at 19:54
No one knows just how the human brain identifies the "good" moves; and it seems that such pattern recognition problems may require fundamentally new algorithm ideas. Another issue is that proving theorems is certainly NP-complete. Your graph of theorems will grow large very quickly with proof-length, such that it could not be stored within the observable universe if it's to include all theorems with medium-length proofs. I'm sure the Poincare Conjecture is beyond the reach of brute force. But if there is ever a computer emulating Euler's brain, I would love to see what it spits out! –  Jonas Kibelbek Apr 17 '12 at 20:10
Still, computers are able to solve at least some problems (see Coq for example). The question is, if i understand it correct, "when the computers will be able to invent new problems, such that I will consider useful". The problem there is that the OP does not even know for themselves what they will consider useful and what they will not, but still want the computer to do such a job. –  penartur Apr 18 '12 at 5:27
All the protons in the visible universe will have decayed long before you enumerate even the one-page proofs (unless you use a really large font size). BTW, "true" and "provable" are not the same; you can't enumerate the true statements, only the provable ones. –  Robert Israel Apr 18 '12 at 6:11
@JonasKibelbek, NP-hard, not NP-complete. There are certainly some theorems whose proof is exponentially larger than the theorem, so theorem proving isn't in NP. –  Peter Taylor Apr 18 '12 at 9:00

They already do. For example, Four color theorem has been proved with a major assistance from a computer. There is a number of theorem provers such as Coq.

As for discovering important mathematics theorems, you have to define what "important" is for you first. Discovering some theorems is not a big deal and could be easily implemented by-hand; there is a set of basic axioms and deduce rules, so it is possible to enumerate all the valid proofs one-by-one, printing the statements they lead to.

-
I somewhat disagree, proving the theorem was reduced to coloring a finite set of maps so it was convenient. imho you can say the mathematicians did over $99.9%$ of the work proving this theorem –  Belgi Apr 17 '12 at 9:35
Someone have to write the program anyway, and the CPUs design itself could be traced back to mathematics; there is always some trace of mathematicians; so you can always say "the matematicians did over 99.9% of the work proving this theorem"; and the only unquestionable counter-example would be some theorem proven by a computer from a self-generated computers' civilization from a galaxy far far away which has nothing to do with humans. Getting back on topic, i don't think we will discover such a civilization within a following 20 years :) –  penartur Apr 17 '12 at 9:48
How about the discovery of a theorem by a computer? –  Makoto Kato Apr 17 '12 at 10:10
First you have to define what is the "theorem". The difference between the theorem (in its common sense) and any other statement following from the axioms is only in their perception by a human - that is, theorem must be "simple" and "interesting". In that sense, "discovery of a theorem by a computer" sounds like "writing of a novel by a computer". Computers write novels, just not of the sort you like :) For example, will the "theorem" stating that $a*b*(c+d+e) = a*b*c+a*b*d+a*b*e$ satisfy you? I doubt that; but it is a theorem nevertheless. –  penartur Apr 17 '12 at 10:15
Computers can do or find useful things though they don't "understand" the usefulness of those things. –  Makoto Kato Apr 17 '12 at 10:55