Why is it so difficult for a computer to prove something?

Question

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

Answer 1

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 2

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.