11. Applications
Society for Industrial and Applied Mathematics eBooks · 2009
11.1 Computer-Assisted Proofs Any computation using IA, and rigorous methods of interval analysis, proves something. The intervals found by the computer will, by construction, certainly contain the results they are constructed to contain. Because of the rigor of interval computation, it is finding use in computer-aided proofs in mathematical analysis, among other areas [42]. Interval analysis has been used, for example, in computational parts of a proof of Kepler's Conjecture on the densest packing of spheres. The following is quoted from Szpiro [240]: The fascinating story of a problem that perplexed mathematicians for nearly 400 years. In 1611, Johannes Kepler proposed that the best way to pack spheres as densely as possible was to pile them up in the same way that grocers stack oranges or tomatoes. This proposition, known as Kepler's Conjecture, seemed obvious to everyone except mathematicians, who seldom take anyone's word for anything. In the tradition of Fermat's Enigma, George Szpiro shows how the problem engaged and stymied many men of genius over the centuries—Sir Walter Raleigh, astronomer Tycho Brahe, Sir Isaac Newton, mathematicians C. F. Gauss and David Hilbert, and R. Buckminster Fuller, to name a few—until Thomas Hales of the University of Michigan submitted what seems to be a definitive proof in 1998. Another proof that used interval arithmetic for rigor was that of the “double bubble conjecture.” It had been conjectured that two equal partial spheres sharing a boundary of a flat disk separate two volumes of air using a total surface area that is less than any other boundary. This equal-volume case was proved by Hass et al. [71], who reduced the problem to a set of 200,260 integrals, which they carried out on an ordinary PC. Warwick Tucker has given a rigorous proof that the Lorenz attractor exists for the parameter values provided by Lorenz. This was a long-standing challenge to the dynamical system community and was included by Smale in his list of problems for the new millennium. The proof uses computer estimates with rigorous bounds based on interval analysis.