Application of computers in higher mathematics

There might be an AI wiki where this question would be appropriate (not saying it is inappropriate here). People like Ray Kurzweil, who is currently working on making search at Google "more intelligent", have claimed that within $5$ years you will be able to ask Google a research level question, and have it come back with an answer in $2$ months say. This sort of thing will be achieved by scouring the internet for information which Ray claims it will be able to understand on some level, rather than just index, and putting the pieces together to reach a conclusion.

If there is a mathematical theorem which can be pieced together in some way from available mathematical knowledge, but perhaps requires a big picture point of view that no human has at the moment, the theorem may be accessible to such a computer. If Ray is correct, then you may expect to see such things.

Of course, further out (into the future) most computer scientists and many neuroscientists see no reason that computers can't eventually achieve and then surpass human level intelligence, at which point you might expect to see them engage in all the same activities that we do, including proving mathematical theorems.

Real people navigate complex situations like mathematical research using metaphorical or visual thinking and honed intuition developed through experience. A lot of it is unconscious reasoning that we form ad hoc rationalizations for upon demand - part of mathematical training is being able to polish such mindstuff into abstract, logical arguments. Part of what makes proofs beautiful, when they are beautiful, is that they 'get to the heart of things' and illustrate why things are the way they are. (Proofs aren't always conceptual and illustrative - they can be also by dry, tedious and unenlightening, and sometimes they can be elegant instead because they cleverly sidestep any requirement to see what's going on.)

Computers won't have the same kind of creative process. However, surely we could be able to make them guided by some kinds of non-arbitrary processes that makes their search more fruitful than random brute search through spaces of strings of symbols (which would presumably be inefficient to the point of being a worthless endeavor). Additionally, a computer's type of creative searching might be able to find things that humans weren't able to find before it.

I think it's unlikely computers will be able to creatively solve the problems mathematicians believe are the greatest, like the millenium problems or Fermat's last theorem or the classification of finite simple groups, even if they can aid us in rote calculations like for the four color theorem. However this is just idle futuristic speculation about how close we can (and will) get computers to simulate human or similar thinking (qualitatively), and I don't think there are any definitive facts at hand.

Computer calculations can do more than rote checks (proof by exhaustion), though. They can do symbolic validation, for example on solutions to the quantum three-body problem of the hydrogen molecule-ion, or find serendipitous numerical patterns that can later lead by human effort to new results, like the BPP formula for digits of $\pi$ or the Lorenz attractor or Feigenbaum constant. See the Wikipedia article on experimental mathematics for more information.

The last question seems to fall under the purview of cognitive psychology of mathematics. I think most of the work in this area has been done on more innate thinking present in children and geared towards analyzing educational outcomes and strategies. However some surely is aimed at higher mathematics and what brain structures are responsible for what mathematicians do and how the relevant mental processes can be modeled.

Real people navigate complex situations like mathematical research using metaphorical or visual thinking and honed intuition developed through experience. A lot of it is unconscious reasoning that we form ad hoc rationalizations for upon demand - part of mathematical training is being able to polish such mindstuff into abstract, logical arguments.

This is a very good point. Our brains use a lot of heuristics to make decisions. If presented with more options than you can thoroughly evaluate in a given timeframe, your brain will use a heuristic to prune. Say you're at dinner and trying to cut calories. Can you realistically thoroughly evaluate every menu item for potential taste and caloric values? Not really. So you use heuristics to make the decision in a reasonable timeframe that you're not holding everyone up. We see this in neuroeconomic models.

Could a computer be programmed to solve Millennium Prize Problems on its own for example? If that is too ambitious, then could it assist a mathematician in solving them in a more useful way than merely computing?

I'm pretty sure not. I think this goes back to Godel's incompleteness theorems, for the P = NP problem. I think by Godel's second incompleteness theorem, if a Turing Machine could prove P = NP, then the Turing model would be inconsistent. Note that I'm not very well versed on Godel's theorems, so I'm happy to retract this if someone feels I'm off-base on this point.

Much advancement is happening in AI and many companies/universities are trying to delegate human abilities like driving a car, walking, conversing, etc. to computers so why wouldn't they be able to delegate the skills of a mathematician?

Walking and driving deal a lot with path-finding. It's fine-tuned graph theory. Conversing is an area in which I'm not overly familiar. A lot of it deals with Natural Language Processing and Data Mining, though. That's a far cry from stating something axiomatic or proving something non-trivial.

Considering that mathematics is a deductive system, if a computer became able to prove things like a mathematician would, starting with axioms and deriving new properties, where could this lead if a computer worked on deriving new theorems non-stop for sometime? Will it ever hit a brick wall and become unable to make progress?

Let's consider something else. How often do people (including mathematicians) get it wrong? If computers have a mathematician's ability, how will we know when computers are wrong? How will we weed through all the mathematics produced by a computer if it is on the order of gigabytes or terabytes?

http://en.wikipedia.org/wiki/Automated_theorem_proving

http://en.wikipedia.org/wiki/First-order_logic

The short answer to your question is, "yes" there are many computer programs that can solve and check mathematical proofs for validity of the proposition and of the proof itself. Mathematicians have been designing programs like this pretty much as long as computers have been around. Computer programs are especially good at solving first-order logic problems and there are many ways (described in the article) to reduce higher-order logic problems down to first-order. So from a purely conjecture-proof standpoint computers are quite capable of solving problems. When it comes to putting in a research question and getting a PhD thesis or journal article out of a computer with no human assistance, well that would put a lot of researchers out of work so it probably wouldn't be in their best interest to figure out how to do that lol.

"Gödel's completeness theorem states that the theorems (provable statements) are exactly the logically valid well-formed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven." However, one problem is that if the conjectures are not valid then the computer would just keep working and neither the computer (nor the operator perhaps) would know when to terminate the program.

One of my old professors has a theorem solver for some specific sets of axioms: http://math.boisestate.edu/~holmes/marcel.html

Journal of Automated Reasoning: http://link.springer.com/journal/10817

The stuff in that journal is beyond me, but it's interesting to read the abstracts.