Computer-Assisted Proof

Computer-assisted proof refers to the relatively new concept of using a significant computational component in a rigorous mathematical proof. The Four Color Theorem is the breakout example of a result proven with computer assistance; its proof was so controversial (see, e.g., the last chapter in this book) that two researchers later completed a project to formally verify the proof in painstaking detail.

Since then many more problems have been resolved using computer proof, including the Kepler conjecture, existence of the Lorenz attractor (Smale's 14th problem), and the solution of checkers. Even so, the role of computer-assisted proof remains somewhat contentious.

I am particularly interested in situations where it is not immediately obvious that a computer can be used for rigorous proof. (By contrast, it was never in question that, in theory, a computer could solve checkers. Of course, making that a reality still required impressive work.) One tool I use for such problems is an effective form of the inverse function theorem (which can alternately be viewed as a fixed point theorem). Loosely put, this theorem says that if a point can be found which approximately satisfies a system of equations, then there is an exact solution nearby. This theorem can even be used in an infinite-dimensional Banach space, which is a central mathematical component of my gravitational choreography project.

I developed a software package, called QNewton, for rigorously proving existence of solutions to systems of polynomial equations. QNewton is a C++ library with a Python frontend. It has special support for equations over the complex numbers, quaternions, and octonions. It uses a damped Newton's method algorithm, computed by LAPACK, to find an approximate solution. It then proves existence of a nearby solution by using interval arithmetic, as provided by the MPFI library, to bound the inverse of the Jacobian. Below is a transcript of a session using QNewton to find two orthogonal unit vectors over H. It finds an approximate solution and certifies that an exact solution exists within 10^-15 of what is printed.