Computer calculations in a paper

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


          Inequality
          (from p.11 of the arXiv version.)
Their abstract begins:

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.


Look at interval arithmetic. Warwick Tucker used this to prove Smale's fourteenth problem, which is a pretty good precedent for its use in a proof.


This is a problem that I have faced also. One approach is to try to prove rational polynomial bounds on the relevant functions (by Taylor series with remainder, for example) that are accurate enough to satisfy the same inequalities. Then you can prove the inequalities rigorously by various methods; the paper of Solovyev and Hales that Joseph links to describes free software better than I knew of before. If the functions vary too much you might need to subdivide the domain and apply the method separately to each part.

You will then face the problem of what to put in the paper, as nobody wants to see page-long intermediate expressions. But at least you can describe how you went about constructing a rigorous proof.

Tags:

Journals