I come across a system of polynomial equations. Although I can solve it by Mathematica (numerically), I wonder whether it is possible to prove this root indeed exists. Any general method to do it? For example, $f(x_1,x_2)=0$ ; $g(x_1,x_2)=0$ ; $f$ and $g$ are polynomials of $x_1$ and $x_2$, and I compute an approximate root $(x_1^*,x_2^*)$ by some numerical method. How can I show there indeed exists a root around this approximate calculated root? I just wonder whether there exist some general theories in doing so.

$\begingroup$ Real root or complex root? How many equations/unknowns? $\endgroup$ – Igor Rivin Oct 6 '16 at 10:54

$\begingroup$ real and two equations with two unknowns $\endgroup$ – stephenkk Oct 6 '16 at 11:19

1$\begingroup$ Could you perhaps tell us the system? In some cases you can guess the exact algebraic solution after you solved the system to high accuracy and then check the algebraic solution in exact arithmetic. Sometimes Smale's Alpha Theory helps. $\endgroup$ – Moritz Firsching Oct 6 '16 at 13:04

$\begingroup$ I have the impression that in the zerodimensional case that Grobner bases plus picking out the real solutions works better. $\endgroup$ – arsmath Oct 6 '16 at 13:59

$\begingroup$ @arsmath I am not sure, but it is certainly true that the zerodimensional case is special... $\endgroup$ – Igor Rivin Oct 6 '16 at 14:33
For polynomials you can, though the details are technical. For a single univariate polynomial you can use the technique of Sturm sequences to find out how many real roots there are, and put bounds on the roots. For a system of that has finitelymany solutions, you can use the theory of Grobner bases to find all complex solutions, and then there are special techniques to pick out the real solutions. Sturmfels' book has details in chapter 4.
In theory you can do it even if you have infinitely many solutions, though it's much much harder. This goes under the name of Tarski's quantifier elimination for real closed fields.

$\begingroup$ The cylindrical algebraic decomposition mentioned by Igor Rivin is a more computationally efficient quantifier elimination algorithm than Tarski's. $\endgroup$ – Timothy Chow Oct 7 '16 at 2:51

$\begingroup$ I used to be in computer algebra, and back then people used "quantifier elimination" for any algorithm to decide the theory of real closed fields, including CAD. That was a while ago, so maybe that usage as died out, or maybe I hung out with a bunch of weirdos. (It was only a long time later that I learned that "quantifier elimination" was a general concept in model theory.) $\endgroup$ – arsmath Oct 7 '16 at 5:59