•  Listen

CAPA – Computer-aided proofs in analysis

Aims

Our research aims at advancing the frontiers of computer-aided proofs in mathematical analysis. This area of research is geared to deal with problems that cannot be solved by traditional mathematical methods alone. Typically, such problems have a global component as well as a non-linear ingredient. Hard problems of this type have traditionally been studied through numerical computations alone, and therefore our knowledge of these lack the rigour demanded by a mathematical proof. Our research aims to bridge the gap between a numerically observed phenomenon, and its mathematical counterpart.

Methods

Bringing computers into the mathematical framework of a proof is achieved by developing a means of computing numerically yet with mathematical rigour – validated numerics. The underlying arithmetic is set-valued, and is based on the inclusion principle that enables us to enclose the image of a function or operator. By carefully designing the numerical method, we can ensure that the result of the original problem is enclosed in the set-valued output of the program.

Applications

Many important areas of application involve non-linear dynamics. Some examples are parameter estimation for biochemical systems, existence proofs for viscous shock solutions for hyperbolic conservations laws, locating and/or counting limit cycles for planar vector fields, as well as advanced studies of higher-dimensional dynamical systems displaying chaotic motion. These categories of problems all share the same inaccessability due to the non-linearities that affect the global behaviour of the underlying system.