# 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. – Yuval Filmus Apr 15 '18 at 11:48
• @YuvalFilmus. Thanks! So what kind of problems can be solved automatically? – Math-fort Apr 15 '18 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. – Yuval Filmus Apr 15 '18 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... – Discrete lizard Apr 15 '18 at 14:52
• "(a + b)^2 == a^2 + b^2 + 2ab" on WolframAlpha – Nat Apr 16 '18 at 0:39