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.

-bash-4.2$ python

Python 2.7.3 (default, Jul 24 2012, 11:41:40)

[GCC 4.6.3 20120306 (Red Hat 4.6.3-2)] on linux2

Type "help", "copyright", "credits" or "license" for more information.

>>> import QNewton, random

>>> q = QNewton.Newton()

>>>

>>> q.set_parser_parameters({'n':3})

>>> q.parse_block("""

... y(length_of_v_minus_1) := SUM i = 1 TO n x(v_$i)~ x(v_$i) - 1

... y(length_of_w_minus_1) := SUM i = 1 TO n x(w_$i)~ x(w_$i) - 1

... y(inner_product_of_v_and_w) := SUM i = 1 TO n x(v_$i)~ x(w_$i)

... CONSTRAIN Ry(length_of_v_minus_1)

... CONSTRAIN Ry(length_of_w_minus_1)

... CONSTRAIN y(inner_product_of_v_and_w)

... """)

>>>

>>> random.seed(0)

>>> for i in [1,2,3]:

... q.initialize_variable('v_'+str(i), [random.gauss(0,1) for e in range(4)])

... q.initialize_variable('w_'+str(i), [random.gauss(0,1) for e in range(4)])

...

>>> q.Newton_steps(20)

1.1102230246251565e-16

>>> print q.get_variables(['x(v_'+str(i)+')' for i in [1,2,3]])

[[0.4515263508773185, -0.43936811088449534, -0.6219617443506098, 0.09770788700877156], [-0.4294481290522128, 0.3416675686795149, 0.36230284325540785, 0.07287513389077427], [1.0632934395276348, -0.3844692946079836, 0.2952430393273164, -0.6351234425427567]]

>>> print q.get_variables(['x(w_'+str(i)+')' for i in [1,2,3]])

[[-0.8901934613748367, 0.08285079510389272, -0.22802449412824322, -0.23962866358005525], [-0.08085155541422835, 1.0285395568189042, -0.0377382252039173, -0.513058875975375], [-0.1298925993149464, 0.6588293120641708, 0.09001291506476068, -0.5505993355077293]]

>>>

>>> q.prepare_rigorous()

5.619502137824812e-17

>>> q.do_rigorous(1.0e-15)

'Success'