Computer-assisted proofs - tools, methods and applications

Motivation

The seminar is intended to assemble a diverse group of scientists working on differing aspects of computer assisted proofs and verification methods.

Computer assisted proofs in general are characterized by the fact that part of a mathematical proof is assisted in an algorithmic way. This includes numerical calculations, taking account of all numerical errors, as well as symbolic manipulations.

This concept of computer assisted proofs can be regarded as a special approach to constructive mathematics. In recent years, various mathematical problems have been solved by computer-assisted proofs, among then the Kepler conjecture (a 3 dimensional sphere packing problem), the existence of chaos, the existence of the Lorenz attractor, and more.

In the SIAM News 1-2/2002, Lloyd N. Trefethen (Oxford) proposed a 10x10 digit Challenge. These are ten difficult numerical problems with a single number as result. The problems vary from global optimization, numerical integration, partial differential equations to probabilistic problems and more. The challenge was to produce 10 correct digits of each solution. Various researchers participated in the contest, but only few of them could give correct answers. An outstanding approach, winning the contest, was the result of effort by a group of four researchers from four different countries. Remarkably, five out of the ten problems were solved using verification methods and the MATLAB toolbox INTLAB for reliable computing, developed by the fourth organizer.

A major problem in Computer Algebra which stimulated a tremendous amount of research is quantifier elimination. Tarski's algorithm with polynomial equations and inequalities over the real numbers has rendered decidable many problems, including optimization problems in real geometry and real algebra. Collins's cylindrical algebraic decomposition algorithm of the arising semi-algebraic sets gives a general purpose solver. However, Tarski's general theory is exponential space hard, and implementations of Collins's algorithm have exposed the difficulty of the arising exact algebraic number arithmetic.

However, large subsets of Tarski's theory are polynomial-time decidable, such as semidefinite programming (SDP). SDP and problems solvable by Newton iteration have efficient implementations including validated results. And here is the bridge to computer-assisted proofs.

That interplay between approximate and exact algebraic number arithmetic has recently lead to irrefutable computer proofs of real optimization problems that were unachieved before. A purpose of our seminar is to explore those new directions in real optimization and quantifier elimination.

With the seminar we intend to bring together researchers from various fields with the common interest to produce reliable results on digital computers. This covers exact methods from computer algebra, numerical algorithms with result verification as well as so-called error-free transformations, recently a rapidly growing field. Here floating-point arithmetical operations do not only produce an approximation but the exact error as well. Successive application of such error-free transformations allows to produce reliable results very rapidly.

The participants will come from different fields, use different methods and have different view points, but are united by the common goal. And this is exactly the appeal of the seminar, the interaction between the different fields by demonstrating achieved solutions, by searching for new applications of existing methods, and vice versa, by posing open problems arising in applications. For this purpose we want to invite in particular a number of young scientists to introduce them to and generate interest in other fields. The choice of organizers also reflects different fields of interest and expertise. The stimulating atmosphere in Dagstuhl is definitely a fruitful environment for this enterprise.