18
$\begingroup$

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), 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" ?

$\endgroup$
  • 7
    $\begingroup$ 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. $\endgroup$ – Dave Clarke Jun 26 '11 at 15:40
  • $\begingroup$ @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...) $\endgroup$ – Max Muller Jun 26 '11 at 15:56
  • $\begingroup$ 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? $\endgroup$ – Max Muller Jun 26 '11 at 15:57
  • 7
    $\begingroup$ 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" (math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html). Zeilberger's frequent coauthor, Shalosh B. Ekhad, is a computer. $\endgroup$ – Rob Simmons Jun 26 '11 at 16:04
  • 4
    $\begingroup$ The following question also gives several nice examples of computers helping to prove theorems: cstheory.stackexchange.com/questions/82/… $\endgroup$ – Mugizi Rwebangira Jun 28 '11 at 13:00
22
$\begingroup$

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.

$\endgroup$
18
$\begingroup$

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, 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 describes how the proof assistant Coq is used to prove the four colour theorem. Mechanized mathematics (overview ) 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 employs model checking and model finding to good effect, and it's quite usable.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Max Muller Jul 7 '11 at 16:01
  • $\begingroup$ You win some, you lose some. $\endgroup$ – Dave Clarke Jul 7 '11 at 17:31
  • $\begingroup$ A less technical, more mathematical account 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). $\endgroup$ – huitseeker Jul 8 '11 at 10:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.