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 - The Fusion of Science and Community**

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

Loading...

Similar Threads - Capabilities Automated Theorem | Date |
---|---|

I An easy proof of Gödel's first incompleteness theorem? | Mar 6, 2018 |

A How does it not contradict the Cohen's theorem? | Sep 15, 2017 |

Automated shifting correlation test | Jun 16, 2012 |

How to semi-automate proofs? | Dec 24, 2007 |

**Physics Forums - The Fusion of Science and Community**