From the introduction: A classical mathematical proof is constructed using pencil and paper. However, there are many ways in which computers may be used in a mathematical proof. But ‘proof by computer’, or even the use of computers in the course of a proof, is not so readily accepted (the December 2008 issue of the Notices of the American Mathematical Society is devoted to formal proofs by computer).
In the following we introduce verification methods and discuss how they can assist in achieving a mathematically rigorous result. In particular we emphasize how floating-point arithmetic is used.
This review article is devoted to verification methods and consists of three parts of similar length. In Part 1 the working tools of verification methods are discussed, in particular floating-point and interval arithmetic; my findings in Section 1.5 (Historical remarks) seem new, even to experts in the field.
In Part 2, the development and limits of verification methods for finite-dimensional problems are discussed in some detail. In particular, we discuss how verification is not working. For example, we give a probabilistic argument that the so-called interval Gaussian elimination (IGA) does not work even for (well-conditioned) random matrices of small size. Verification methods are discussed for problems such as dense systems of linear equations, sparse linear systems, systems of nonlinear equations, semi-definite programming and other special linear and nonlinear problems, including M-matrices, finding simple and multiple roots of polynomials, bounds for simple and multiple eigenvalues or clusters, and quadrature. The necessary automatic differentiation tools to compute the range of gradients, Hessians, Taylor coefficients, and slopes are also introduced. Concerning the important area of optimization, A. Neumaier gave in his article [Acta Numerica 13, 271–369 (2004; Zbl 1113.90124)] an overview on global optimization and constraint satisfaction methods. In view of the thorough treatment there, showing the essential role of interval methods in this area, we restrict our discussion to a few recent, complementary issues.
Finally, in Part 3, verification methods for infinite-dimensional problems are presented, namely two-point boundary value problems and semilinear elliptic boundary value problems.
Throughout the article, many examples of the inappropriate use of interval operations are given. In the past such examples contributed to the dubious reputation of interval arithmetic (see Section 1.3), whereas they are, in fact, simply a misuse.
One main goal of this review article is to introduce the principles of the design of verification algorithms, and how these principles differ from those for traditional numerical algorithms (see Section 1.4). Many algorithms are presented in executable MATLAB/INTLAB code, providing the opportunity to test the methods directly. INTLAB, the MATLAB toolbox for reliable computing, was, for example, used by F. Bornemann, D. Laurie, S. Wagon and J. Waldvogel (2004; Zbl 1060.65002) in the solution of half of the problems of the SIAM \(10\times 10\)-digit challenge by N. Trefethen (2002).