- #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:
Thanks for the insights!
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!