# Could computers someday discover theorems or find demonstrations?

Cloud computing and quantum computers bring computers to what seems like a limitless calculation power?

If one sees all the mathematical operations and theorems as a toolset that a computer can use, bringing the adecuate automatic or interactive algorithm, it's easy to imagine that some day computers could "brute-force" the discovery of new theorems, for instance.

Take the Pythagorean theorem, someone could measure the sides of a right-angled triangle, and give the input to the computer. Then the computer could give the theorema's formula, and some demostrations.

-
Yes, in fact they started doing so many years ago. en.wikipedia.org/wiki/Automated_theorem_proving – Alex Becker Dec 24 '12 at 0:51
– Andrés E. Caicedo Dec 24 '12 at 1:10
– Andrés E. Caicedo Dec 24 '12 at 1:11
@AndresCaicedo It seems the the answer is yes, computers already do so. My concern is now how to do when computers findings are impossible to verify by humans‌​. I'm afraid the question could be closed, but it is more a mathematics related question that a computer science's one. – rraallvv Dec 24 '12 at 1:28
Theorem discovery is something computers have had some small measure of success doing.... in addition to theorem proving. See doc.ic.ac.uk/~sgc/html_papers/colton_ijcar01.html – Badri Dec 12 '14 at 9:02

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

-

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.

-
For a colorfully presented dissenting opinion, I would suggest googling and browsing the (capital-O) Opinions of Doron Zeilberger... – Tabes Bridges Dec 24 '12 at 1:05
(+1) for BS Theory! – Shaun Ault Dec 24 '12 at 1:15
@IttayWeiss The implications are huge, think for instance in computers finding the "theory of everything"... and when computers reach the Technological singularity we have to trust them a closed eye even when their findings are impossible to verify by humans – rraallvv Dec 24 '12 at 1:20
I don't understand what your comment is trying to say rraallvv. – Ittay Weiss Dec 24 '12 at 1:24
@IttayWeiss I'm saying that if computers are able to do that, there are huge implications, not just "useless activities" – rraallvv Dec 24 '12 at 1:35