# Capabilities of Automated Theorem Provers

1. Feb 2, 2014

### Mathematicize

What are the current capabilities of modern Theorem Provers? I know about logic/undecidability/complexity theory so go ahead and use that jargon. Anyway, I am interested as to why Theorem Provers are not talked about (at least not by math professors). Why have I not heard the following sentence: "This theorem could be a bit tricky to see, but we could always just plug it into our theorem prover."

There are a few valid reasons I can see why not:
1. 1. Godel's incompleteness theorem -- but still maybe the theorem prover can lead you in a direction and give you new ideas that you were not previously thinking about before?
2. 2. Math professors (including Theoretical Computer Scientists) are not computer savvy enough to get a theorem prover to work.
3. 3 It is very impractical to use one, because you have to give it an entire axiom list and other known lemmas/theorem. By the time you did all of this, you could have solved the problem for yourself.

Thanks for the insights!

2. Feb 3, 2014

### Office_Shredder

Staff Emeritus
The main problem is that theorem provers have to enumerate faaaar too many proof attempts before they can get at one that works. If you have three different things you can do at each step, and your proof is going to be 5,000 steps, and you can logically test a proof every 1/1000th of a second, you will take something on the order of 10^(2374) years to test all the possible proofs before you hit the right one.

The kinds of theorems that theorem provers solve are ones that a human can do in a couple of lines; the ones that humans have trouble with are ones that theorem provers are just not capable of doing at this point in time. Certainly anything that is a research level problem for the most part is going to be completely out of the realm of a theorem prover; the first step in any paper is to pull on hundreds of years of mathematical development that a theorem prover is going to have to recreate from scratch. There are examples of problems that have been solved by use of a theorem prover, but each time a lot of work and understanding of the problem needs to go into developing the theorem prover so that it has exactly the right list of assumptions to iterate through, with no useless information and being equipped with the state of the art tools that are probably going to be needed to solve the problem.

As far as using it for educational purposes, anybody interested in research level mathematics is not learning a collection of theorems, but learning how to prove things. The proof of something is more important than the actual statement of the theorem most of the time. If you are not learning for research purposes, then the proof is usually just omitted if it is deemed unimportant to educational purposes. Being told a theorem prover could do it contributes nothing in either case.

As an example of the failure of theorem provers, the Millennium prizes come with a 1,000,000 dollar prize attached to them. If a theorem prover could generate a proof of these problems (one of which has been solved, so it is possible in at least one case) then somebody would just go ahead and solve these problems and make a lot of money, and a LOT of academic fame in the process. The simplest explanation here is the correct one; theorem provers are not capable of generating mathematics at the highest levels at the moment.

3. Feb 3, 2014

### jgens

A beautiful essay that is at least peripherally related is On Proof and Progress in Mathematics by Bill Thurston (http://arxiv.org/abs/math/9404236). One of the key points he stresses is the importance of human comprehension. Of course we are interested whether our theorems are true, but more so, we wish to understand why they are true. It's fairly short, so if you have the time, I definitely recommend reading it.

4. Feb 4, 2014

### FactChecker

I have seen a theorem prover solve some interesting example problems. In a logic class it would be interesting to learn how they work. Unfortunately, the one I saw they don't output intermediate results that would give any insight into the proof. It just said that it succeeded or it gave you a counterexample. For the "proof", you had to take it's word for it. An example of an entertaining use is to ask it to prove that there is no solution to a particular Sudoku problem. Then it will give you a counterexample that is a solution.

5. Feb 5, 2014

### Hornbein

I haven't look at this for twenty years or so, when I was going back to grad school and had to choose between something like this and mathematics.

Doug Lenat of Carnegie Mellon had written a book on automated theorem proving. I knew a computer science professor from there who told me that the inside word was that the research was bogus.

I was traveling around the US and interviewing grad school students. Automated theorem proving was so out of style that a number of them had had their professors quit the field, abandoning the students. Very bad.

By the way, the emphasis wasn't on getting a computer to find original proofs. I think that this is way beyond what can be attempted today. It was on checking existing proofs, which is a more reasonable goal.

If you can convince a computer that your theorem is correct then it very likely is. What's more than that, I've been told that most published proofs have at least minor errors. The trouble is that a) a great deal of boring labor is involved. b) people don't like being told that their proof is incorrect c) in the few cases that proofs have been checked they were found to be correct, so it seemed like a waste.