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. 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!