Could computers someday discover theorems or find demonstrations?

Solution 1:

In a loose sense they already have:

• Prover9, for example, can be fed in "axioms" and "goals" and can (hopefully) deduce the goal from the input axioms. Importantly, this still requires human input.

  • For important results (which are usually out of the reach for automated theorem provers directly), usually a human operator divides the result into a sequence of intermediate goals that the software can handle.
  • This method can be useful when you have to prove a large number of trivial theorems (which would be too tedius for humans to do). For example, when you want to classify varieties that satisfy short identities (e.g. this; PDF warning).

Doron Zeilberger has taken the idea of automated theorem proving even further, and has programmed the computer to automatically conjecture and prove results (e.g. 3x+1-like conjectures: ref.).

I think, in the not-too-distant future, we will see computers automatically (a) finding counter-examples to human-created "theorems", and (b) proving respectable conjectures. Two major obstacles are:

• Automated theorem provers are somewhat limited to first order logic, whereas humans are not.
• Humans, when proving things, can consult the literature, which is written in "human".

I think, in the future, advances in machine learning, data mining, and natural language processing will enable automated theorem provers to "learn" lemmata (and find conjectures) from the internet, and automatically use them in a proof. This would be a way computers could "cheat", so they don't need to limit themselves to theorems proved only by first-order logic.

I think the most likely area that automated theorem provers will begin to compete with humans in non-trivial ways will be abstract algebra. It's somewhat already started (see this; PDF warning).

Solution 2:

First, let me mention that computers already find new theorems and proofs. In the past years a lot of progress was made in the area of research involving automated theorem provers and proof verifiers (the system Coq, http://coq.inria.fr/, is perhaps the most important one).

Even before this very powerful system a computer program was set up, was fed the axioms of Euclidean geometry, and started spitting out theorem after theorem, with complete derivations. Some of these proofs were new proofs (or forgotten proofs) to well known theorems. Some of the theorems were undoubtedly new, but it is questionable what their worth or interest was.

One needs to understand that doing mathematics does not involve randomly proving new statements that follow from the axioms of any particular system. Nor does a mathematician wake up in the morning, chooses a random set of new axioms, calls the resulting structure BS, and starts proving stuff about such BS's. Such a thing will rightfully be called "BS theory".

Computers are already far better than humans at both of these useless activities. However, when doing mathematics there is some aim in mind. A goal that justifies the particular symbolic manipulations, rendering them far from arbitrary. Computers today can aid mathematicians sometimes when developing new theories or in finding new theorems. Computers can certainly help verify, sometimes very complicated, proofs. But there is today still no indication that (at least in the near future) computers will be able to just on their own produce new pieces of interesting and meaningful mathematics.