Informal and formal verification of nonlinear inequalities with applications to discrete geometry

Informal and formal verification of nonlinear inequalities with applications to discrete geometry

-
Tom Hales , University of Pittsburgh Mellon
Fine Hall 224

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.