Can I prove following statements with available automated theorem provers?
1- $(a+b)^2=a^2+b^2+2ab$.
2- $if\; 11|2a-3b \;\; then\;\; 11|7a-5b $.
3- $if\; x^2+ax+b=0\;\; then\;\; x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$.
4- if a is even then 4a is also even.
and so on!
I am asking this question because I just found the application of ATPs in proving theorems in logic.
Most automated theorem provers nowadays have as a subcomponent SMT solvers, or often you can use an SMT solver of your choosing with the automated theorem prover. SMT solvers start with a Boolean satisfiability solver (a SAT solver) and extend that with theories, usually decidable, so the propositions can be interesting statements. Basically, a SAT solver only cares about a true/false assignment to the propositions, so as far as it's concerned, they are just opaque atomic propositions. An SMT solver provides that true/false assignment by using a decision procedure for some theory. As the Wikipedia page illustrates, we have decision procedures for quite a few theories at this point.
At any rate, your first problem can be formulated as a problem in a variety of decidable theories including just uninterpreted functions. Often there are special "ring" theories that can solve problems like this efficiently. It is easy to see if two polynomials are equal by just expanding them out and checking whether they have the same coefficients. The second and fourth problems can be viewed as linear algebra problems (over finite fields) or problems in Presburger arithmetic. Either way, they are easily decidable. For the third, it depends on what field you're working over and how you phrase it. For example, a ring solver may readily be able to prove (or may need a bit of inference from the surrounding automated theorem prover) that if $\alpha^2=b^2-4ac$ and $x=\frac{-b+\alpha}{2a}$ then $ax^2+bx+c=0$ simply by substituting and reducing.
The above focused on theories for which we have decision procedures, i.e. algorithms that can answer "true" or "false" to any problem within the theory. Often theories don't have such decision procedures, or they are extremely inefficient. The automated theorem prover (and potentially even the SMT solver) is not limited to decidable theories. In this case, the limitation is mostly on how long you are willing to wait/how much computational resources you are willing to apply to the problem. An automated theorem prover will eventually find any proof or refutation that exists if given enough time and resources. Of course, it's quite possible that the amount of time and resources required may not fit in this universe, and it's much more possible that it won't fit in your budget.
What we're not doing when we use practical automated theorem provers to solve practical problems is writing down the axioms of set theory defining the complex numbers, say, as a set as well as the operations on them, and then attempting to deduce a theorem like $ax^2+bx+c=0 \iff x=\frac{-b\pm\sqrt{b^2-4ac}}{2a}$ directly from the set theoretic definitions. You could do this, but it would take a lot of effort for the automated theorem prover to find a proof. Instead, we abstract as much as possible and often reformulate the problem so that it fits within a decidable theory even if it requires bizarre encodings. Many of the decidable theories are implemented by reduction to other decidable theories. SMT itself is such an example.