<p>Two main difficulties. Incompleteness (see Gödel's Incompleteness Theorems) and the vast size of the search space (there are vastly more uninteresting theorems than interesting ones). Considerable progress has been made using proof assistants (<a href="http://coq.inria.fr/">Coq</a>, Isabelle, Agda, etc). With these the mathematician writes the theorems and lemmas and the proof assistant helps finding proofs and ensures that the proofs are logically valid.</p>

<p>One simple way a computer could prove a new theorem is to take two existing theorems, $P$  and $Q$ and combine them to make the theorem $P\wedge Q$. Of course, if the search procedure is more clever, then you can discover more clever things, but to find something truly interesting and original would require a lot of intelligent tricks and techniques on the part of the programmer. Gödel's incompleteness theorems are relevant here because they place a fundamental limit on what can be discovered within any proof system: a computer could never discover the proof of the consistency of its own logic.</p>

<p>This <a href="http://www.research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf">paper</a> describes how the proof assistant Coq is used to prove the four colour theorem. Mechanized mathematics (<a href="http://www.cas.mcmaster.ca/~carette/publications/JLM_May29_09.pdf">overview</a> ) is one area of TCS devoted to (semi)automatically proving theorems (and in general using computers to help mathematicians). </p>

<p>One area where automated theorem proving (of sorts) is making an impact is in model checking and model finding. Model checking deals with determining whether a given system satisfies a given property, whereas model finding finds a system to satisfy a given collection of properties. The tool <a href="http://alloy.mit.edu/community/">Alloy</a> employs model checking and model finding to good effect, and it's quite usable.</p>

CC BY-SA 3.0
2011-07-07T16:01:06.777Z
I couldn't choose between these two answers, because they're both great. I tossed a coin to decide which one to pick. I'm sorry I didn't pick yours! Thanks a lot anyway.
Max Lonysa Muller
CC BY-SA 3.0
2011-07-07T17:31:30.360Z
You win some, you lose some.
Dave Clarke
CC BY-SA 3.0
2011-07-08T10:56:10.777Z
A [less technical, more mathematical account](http://www.ams.org/notices/200811/tx081101382p.pdf) of the four color proof and its significance was published in a recent AMS notices issue (the whole issue might be advisable reading for people interested in the OP's question).
Francois G
CC BY-SA 3.0
2011-06-26T15:32:23.090Z
2011-06-26T17:34:58.100Z
2011-06-26T17:34:58.100Z
Dave Clarke
<blockquote>
  <p>While there are plans to formalize Fermat's Last Theorem (see this presentation), I have never read or heard that a computer can prove even a "simple" theorem like Pythagoras'. </p>
</blockquote>

<p>In 1949 Tarski proved that almost everything in <em>The Elements</em> lies within a decidable fragment of logic, when he showed the decidability of the first-order theory of real closed fields. So the Pythagorean theorem in particular is not talked about much because it's not especially hard. </p>

<p>In general, the thing that makes theorem proving hard is induction. First-order logic without induction has a very useful property called the subformula property: true formulas $A$ have proofs involving only the subterms of $A$. This means that it's possible to build theorem provers which can decide what to prove next based on an analysis of the theorem they are instructed to prove. (Quantifier instantiation can make the right notion of subformula a bit more subtle, but we have reasonable techniques to cope with this.) </p>

<p>However, the addition of the induction schema to the axioms breaks this property. The only proof of a true formula $A$ may require doing a proof $B$ which is not syntactically a subformula of $A$. When we run into this in a paper proof, we say we have to "strengthen the induction hypothesis". This is quite hard for a computer to do, because the appropriate strengthening can require both significant domain-specific information, and an understanding of <em>why</em> you're proving a particular theorem. Without this information, truly relevant generalizations can get lost in a forest of irrelevant ones. </p>

CC BY-SA 3.0
2011-06-26T21:53:34.027Z
2011-06-26T21:53:34.027Z
Neel Krishnaswami
<p><em>This may be considered a stupid question. I am not a computer science major (and I'm not a mathematics major yet, either), so please excuse me if you think that the following questions display some major erroneous assumptions.</em></p>

<p>While there are plans to formalize Fermat's Last Theorem (see this <a href="http://www.win.tue.nl/diamant/symposium0711/slides/oosterhuisbackup.pdf">presentation</a>), I have never read or heard that a computer can prove even a "simple" theorem like Pythagoras'. </p>

<p>Why not? What is (/are) the main difficulty(/ies) behind establishing a fully autonomous proof by a computer, aided only by some "built-in axioms"? </p>

<p>A second question I would like to ask is the following: Why are we able to formalize many proofs, while it is currently impossible for a computer to prove a theorem on its own? Why is that "harder" ?</p>

CC BY-SA 3.0
2011-06-26T15:40:04.583Z
Two main difficulties. Incompleteness (see Gödel's Theorems) and the vast size of the search space (there are vastly more uninteresting theorems than interesting ones). Considerable progress has been made using proof assistants (Coq, Isabelle, Agda, etc). With these the mathematician writes the theorems and lemmas and the proof assistant helps finding proofs and ensures that the proofs are logically valid.
Dave Clarke
CC BY-SA 3.0
2011-06-26T15:56:05.667Z
@Dave Clarke: ok, so actually you say that a computer *is* capable of proving (new) theorems, but the vast amount of possible searches makes it hard for him/her/it to write a theorem that has any value or is interesting, am I right? Could you please explain why Gödel's Theorems and "Incompleteness" is relevant here? Furthermore, do you have a reference of a research paper or survey article in which it is demonstrated that a computer actually proves a theorem? Lastly, is there a lot of research going on into trying to make computers prove theorems? What is this research area called (cont'nd...)
Max Lonysa Muller
CC BY-SA 3.0
2011-06-26T15:57:46.960Z
and do you know good introductory material on it? What are the prerequisites in both mathematics but especially Computer Science for actually understanding this material?
Max Lonysa Muller
CC BY-SA 3.0
2011-06-26T16:04:59.763Z
You might be interested in some of Dorian Zeilberger's work, such as "*Teaching the Computer how to Discover(!) and then Prove(!!) (all by Itself(!!!)) Analogs of Collatz's Notorious 3x+1 Conjecture*" (http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html). Zeilberger's frequent coauthor, Shalosh B. Ekhad, is a computer.
Rob Simmons
CC BY-SA 3.0
2011-06-26T16:29:29.740Z
One simple way a computer could prove a new theorem is to take two existing theorems, $P$ and $Q$ and combine them to make the theorem $P\wedge Q$. Of course, if the search procedure is more clever, then you can discover more clever things, but to find something truly interesting and original would require a lot of intelligent tricks and techniques on the part of the programmer. Gödel's incompleteness theorems are relevant here because they place a fundamental limit on what can be discovered within any proof system: a computer could never discover the proof of the consistency of its own logic.
Dave Clarke
CC BY-SA 3.0
2011-06-26T16:32:09.363Z
This paper http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf describes how the proof assistant Coq is used to prove the four colour theorem. Mechanized mathematics (overview: http://www.cas.mcmaster.ca/~carette/publications/JLM_May29_09.pdf) is one area of TCS devoted to (semi)automatically proving theorems (and in general using computers to help mathematicians).
Dave Clarke
CC BY-SA 3.0
2011-06-26T16:51:30.290Z
@Dave and Rob: thank you for providing me with some interesting and relevant information. I'm looking forward to reading it.
Max Lonysa Muller
CC BY-SA 3.0
2011-06-26T17:35:19.880Z
I'm compiled my comments together into an answer.
Dave Clarke
CC BY-SA 3.0
2011-06-27T12:47:10.303Z
Two excellent answers, hard to pick one out! I will wait a week. The answer that has the most upvotes by then will be accepted.
Max Lonysa Muller
CC BY-SA 3.0
2011-06-28T13:00:19.437Z
The following question also gives several nice examples of computers helping to prove theorems:                                                                    http://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem
Mugizi Rwebangira
<automated-theorem-proving>
Why is it so difficult for a computer to prove something?
Max Lonysa Muller
# Why is it so difficult for a computer to prove something?

(Asked by: username_0 on 2011-06-26)

*This may be considered a stupid question. I am not a computer science major (and I'm not a mathematics major yet, either), so please excuse me if you think that the following questions display some major erroneous assumptions.*

While there are plans to formalize Fermat's Last Theorem (see this [presentation](http://www.win.tue.nl/diamant/symposium0711/slides/oosterhuisbackup.pdf)), I have never read or heard that a computer can prove even a "simple" theorem like Pythagoras'.

Why not? What is (/are) the main difficulty(/ies) behind establishing a fully autonomous proof by a computer, aided only by some "built-in axioms"?

A second question I would like to ask is the following: Why are we able to formalize many proofs, while it is currently impossible for a computer to prove a theorem on its own? Why is that "harder" ?

**Tags:** automated-theorem-proving

> **Comments:**
> **username_1**: Two main difficulties. Incompleteness (see Gödel's Theorems) and the vast size of the search space (there are vastly more uninteresting theorems than interesting ones). Considerable progress has been made using proof assistants (Coq, Isabelle, Agda, etc). With these the mathematician writes the theorems and lemmas and the proof assistant helps finding proofs and ensures that the proofs are logically valid.  
> **username_0**: @username_1: ok, so actually you say that a computer *is* capable of proving (new) theorems, but the vast amount of possible searches makes it hard for him/her/it to write a theorem that has any value or is interesting, am I right? Could you please explain why Gödel's Theorems and "Incompleteness" is relevant here? Furthermore, do you have a reference of a research paper or survey article in which it is demonstrated that a computer actually proves a theorem? Lastly, is there a lot of research going on into trying to make computers prove theorems? What is this research area called (cont'nd...)  
> **username_0**: and do you know good introductory material on it? What are the prerequisites in both mathematics but especially Computer Science for actually understanding this material?  
> **username_2**: You might be interested in some of Dorian Zeilberger's work, such as "*Teaching the Computer how to Discover(!) and then Prove(!!) (all by Itself(!!!)) Analogs of Collatz's Notorious 3x+1 Conjecture*" (http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html). Zeilberger's frequent coauthor, Shalosh B. Ekhad, is a computer.  
> **username_1**: One simple way a computer could prove a new theorem is to take two existing theorems, $P$ and $Q$ and combine them to make the theorem $P\wedge Q$. Of course, if the search procedure is more clever, then you can discover more clever things, but to find something truly interesting and original would require a lot of intelligent tricks and techniques on the part of the programmer. Gödel's incompleteness theorems are relevant here because they place a fundamental limit on what can be discovered within any proof system: a computer could never discover the proof of the consistency of its own logic.  
> **username_1**: This paper http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf describes how the proof assistant Coq is used to prove the four colour theorem. Mechanized mathematics (overview: http://www.cas.mcmaster.ca/~carette/publications/JLM_May29_09.pdf) is one area of TCS devoted to (semi)automatically proving theorems (and in general using computers to help mathematicians).  
> **username_0**: @Dave and Rob: thank you for providing me with some interesting and relevant information. I'm looking forward to reading it.  
> **username_1**: I'm compiled my comments together into an answer.  
> **username_0**: Two excellent answers, hard to pick one out! I will wait a week. The answer that has the most upvotes by then will be accepted.  
> **username_3**: The following question also gives several nice examples of computers helping to prove theorems:                                                                    http://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem  

---

## 2 answers

### Answer by username_5 on 2011-06-26. Score: 23 | Accepted answer

> While there are plans to formalize Fermat's Last Theorem (see this presentation), I have never read or heard that a computer can prove even a "simple" theorem like Pythagoras'.

In 1949 Tarski proved that almost everything in *The Elements* lies within a decidable fragment of logic, when he showed the decidability of the first-order theory of real closed fields. So the Pythagorean theorem in particular is not talked about much because it's not especially hard.

In general, the thing that makes theorem proving hard is induction. First-order logic without induction has a very useful property called the subformula property: true formulas $A$ have proofs involving only the subterms of $A$. This means that it's possible to build theorem provers which can decide what to prove next based on an analysis of the theorem they are instructed to prove. (Quantifier instantiation can make the right notion of subformula a bit more subtle, but we have reasonable techniques to cope with this.)

However, the addition of the induction schema to the axioms breaks this property. The only proof of a true formula $A$ may require doing a proof $B$ which is not syntactically a subformula of $A$. When we run into this in a paper proof, we say we have to "strengthen the induction hypothesis". This is quite hard for a computer to do, because the appropriate strengthening can require both significant domain-specific information, and an understanding of *why* you're proving a particular theorem. Without this information, truly relevant generalizations can get lost in a forest of irrelevant ones.


---

### Answer by username_1 on 2011-06-26. Score: 18

Two main difficulties. Incompleteness (see Gödel's Incompleteness Theorems) and the vast size of the search space (there are vastly more uninteresting theorems than interesting ones). Considerable progress has been made using proof assistants ([Coq](http://coq.inria.fr/), Isabelle, Agda, etc). With these the mathematician writes the theorems and lemmas and the proof assistant helps finding proofs and ensures that the proofs are logically valid.

One simple way a computer could prove a new theorem is to take two existing theorems, $P$ and $Q$ and combine them to make the theorem $P\wedge Q$. Of course, if the search procedure is more clever, then you can discover more clever things, but to find something truly interesting and original would require a lot of intelligent tricks and techniques on the part of the programmer. Gödel's incompleteness theorems are relevant here because they place a fundamental limit on what can be discovered within any proof system: a computer could never discover the proof of the consistency of its own logic.

This [paper](http://www.research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf) describes how the proof assistant Coq is used to prove the four colour theorem. Mechanized mathematics ([overview](http://www.cas.mcmaster.ca/~carette/publications/JLM_May29_09.pdf) ) is one area of TCS devoted to (semi)automatically proving theorems (and in general using computers to help mathematicians).

One area where automated theorem proving (of sorts) is making an impact is in model checking and model finding. Model checking deals with determining whether a given system satisfies a given property, whereas model finding finds a system to satisfy a given collection of properties. The tool [Alloy](http://alloy.mit.edu/community/) employs model checking and model finding to good effect, and it's quite usable.

> **Comments:**
> **username_0**: I couldn't choose between these two answers, because they're both great. I tossed a coin to decide which one to pick. I'm sorry I didn't pick yours! Thanks a lot anyway.  
> **username_1**: You win some, you lose some.  
> **username_4**: A [less technical, more mathematical account](http://www.ams.org/notices/200811/tx081101382p.pdf) of the four color proof and its significance was published in a recent AMS notices issue (the whole issue might be advisable reading for people interested in the OP's question).  

---

