# What kind of math problems can be solved by automated theorem provers?

Can I prove following statements with using available automated theorem provers?

1. $(a+b)^2=a^2+b^2+2ab$.

2. If $11 \mid 2a-3b$, then $11 \mid 7a-5b$.

3. If $ax^2+bx+c=0$, then $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$.

4. If $a$ is even then $4a$ is even.

and so on!

I am asking this question because I just found the application of Automated theorem provers in proving theorems in logic.

• You can certainly prove all of these (except perhaps 3, which is wrong as written) using all standard proof assistants, though it probably won't be automatic. Apr 15, 2018 at 11:48
• @YuvalFilmus. Thanks! So what kind of problems can be solved automatically? Apr 15, 2018 at 11:51
• You can simplify expressions automatically, though this is a service provided by Computer Algebra Systems. I don't think modern proof assistants can automatically prove anything of substance, though it's better to ask the experts. Apr 15, 2018 at 11:53
• @YuvalFilmus I think that what you say is often true, in the sense that only when an automated proof method gives interesting results, we are willing to call it a part of a CAS... Apr 15, 2018 at 14:52
• "(a + b)^2 == a^2 + b^2 + 2ab" on WolframAlpha
– Nat
Apr 16, 2018 at 0:39