This talk will describe some tools for the automated verification of nonlinear inequalities involving a small number of real independent variables.  Various problems in discrete geometry can be reduced to finite collections of nonlinear inequalities.   In this way computer-assisted proofs of various conjectures in discrete geometry can be obtained.