A tool for formal verification of nonlinear inequalities in HOL Light.

Part of the Flyspeck project:
http://code.google.com/p/flyspeck/

Distributed under the same license as HOL Light.

See docs/FormalVerifier.pdf for additional information.