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."(adsbygoogle = window.adsbygoogle || []).push({});

There are a few valid reasons I can see why not:

- 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. Math professors (including Theoretical Computer Scientists) are not computer savvy enough to get a theorem prover to work.
- 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 Forums | Science Articles, Homework Help, Discussion**

Join Physics Forums Today!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# Capabilities of Automated Theorem Provers

**Physics Forums | Science Articles, Homework Help, Discussion**