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.
The magic words are: Cylindrical Algebraic Decomposition.
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 finitely-many 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.