Return to Answer

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as

We present a formal tool for verification of multivariate nonlinear inequalities. Our verification method is based on interval arithmetic with Taylor approximations. Our tool is implemented in the HOL Light proof assistant and it is capable to verify multivariate nonlinear polynomial and non-polynomial inequalities on rectangular domains.

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397.

they show how to prove inequalities such as

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as