Capabilities of Automated Theorem Provers

In summary, modern theorem proving machines are not as powerful as they once were, and are only really useful for problems that are too hard for humans to solve. They are not very practical for educational purposes, as they require a lot of work to set up and are not very user-friendly.
  • #1
Mathematicize
11
0
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!
 
Physics news on Phys.org
  • #2
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
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
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
Mathematicize said:
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!

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.
 

What are automated theorem provers?

Automated theorem provers are computer programs that are designed to automatically prove mathematical theorems. They use logical deduction to analyze a given set of axioms and rules, and then generate a proof for a given theorem.

What is the purpose of automated theorem provers?

The main purpose of automated theorem provers is to provide a tool for mathematicians and computer scientists to help them prove complex theorems. These tools can save time and effort by automating the process of proving theorems, which can be tedious and error-prone when done manually.

What are the capabilities of automated theorem provers?

Automated theorem provers have the ability to handle complex mathematical expressions and proofs, as well as perform various logical operations such as deduction, induction, and contradiction. They can also handle different types of mathematical structures, such as algebraic structures, geometric structures, and first-order logic.

What are the limitations of automated theorem provers?

One of the main limitations of automated theorem provers is their inability to handle creativity and abstraction. They are limited to the rules and axioms that are predefined by the programmer, and may not be able to think outside of those constraints. They also struggle with problems that require human intuition and reasoning.

How are automated theorem provers used in practical applications?

Automated theorem provers are used in various practical applications, such as software verification, program synthesis, and artificial intelligence. They can also be used in mathematical research, to help prove new theorems or disprove existing conjectures. Additionally, they are used in education to teach students about logic and proof techniques.

Similar threads

Replies
72
Views
4K
  • Set Theory, Logic, Probability, Statistics
Replies
2
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
3
Views
2K
Replies
2
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
6
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
7
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
4
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
918
  • Set Theory, Logic, Probability, Statistics
Replies
10
Views
1K
  • Classical Physics
Replies
1
Views
544
Back
Top