Webrelaunch 2020

Computer-Assisted Proofs and Verification Methods

  • Time: 18.9.2011 - 22.9.2011

Japanese-German Workshop
September 18 - 22, 2011


The 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 them 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 S.M. Rump (TU Hamburg-Harburg).

Many problems involving partial differential equations, with a huge number of applications in science and engineering, allow very stable numerical computations of approximate solutions, but are still lacking analytical existence and multiplicity proofs. In recent years, methods have been developed which supplement purely analytical arguments by computer-assisted approaches, and these methods have turned out to be successful in various examples where purely analytical methods have failed. One of the organizers (Plum) and the Japanese scientists M.T. Nakao and S. Oishi have made internationally recognized contributions by computer-assisted proofs in the field of partial differential equations and their applications, like fluid dynamics (Navier-Stokes problems, Orr-Sommerfeld equation, Rayleigh-Benard heat convection), electro-dynamics (photonic crystals, scattering problems described by the Lippmann Schwinger equation), magneto-hydrodynamics (plasma flow), nonlinear waves (for example, travelling waves in a beam), elasticity/plasticity, variational inequalities, obstacle problems, and semilinear elliptic boundary and eigenvalue problems in general. In this context, various kinds of constants appearing e.g. in finite element error bounds or in Sobolev embeddings are needed explicitly, and have been determined by computations of analytical and computer-assisted means.

S.M. Rump and S. Oishi have extensively developed arithmetic and linear algebra tools for computer assisted proofs based on numerical computations with guaranteed accuracy. For example, they have developed fast and ultra-fast methods for solving numerical linear algebraic problems with guaranteed accuracy, adaptive methods for solving ill-posed problems in numerical linear algebra, accurate summation and dot product algorithms for floating point vectors. These methods are also provided in the aforementioned MATLAB interval toolbox INTLAB for verification algorithms, which is widely used all over the world. As an application of these tools, Oishi and Rump have also developed algorithms in computational geometry, which always give mathematically correct results even if they are executed by floating point calculations.

The particular expertise of Japanese and German scientists indicates that a workshop with participants primarily from Japan and Germany and from all the described subareas will be very promising. We are convinced that our workshop has high potential for very fruitful interactions between these areas. Moreover, it will lead to significant developments in several inter-related fields like numerical functional analysis, ordinary and partial differential equations, ill-posed and ill-conditioned problems, constrained programming, reliable algorithms, and topics related to computer arithmetic.


Kaiserstraße 93, Rooms 1C-04, 1C-01 - Please see map!


G. Alefeld (Karlsruhe), M. Plum (Karlsruhe), S. M. Rump (Hamburg-Harburg)



Top of page