In this section we describe the research at MOX related to methods for computer-assisted proof.
The history of mathematics is very rich of proof of existence, and possibly uniqueness, of solutions for all kind of equations. We consider primarily differential equation, but what follows applies to a wide range of problems.
Except for the rather rare cases when it is possible to construct explicitly a solution, proofs of existence usually rely on very general principles, e.g. variational principles and fixed point theorems. The advantage of such approaches is that they usually require very generic assumptions, and therefore the results apply to a broad class of equations. But this high degree of generality has an inevitable drawback: these methods usually provide very little information on the properties of the solutions.
A computer assisted proof (CAP) has somehow the opposite characteristics: it usually applies to a specific equation or a very small class of equations, but provides very detailed information on the solution.
In a nutshell, a CAP consists of two main steps: finding an approximate solutions of some functional equation and proving that there exists a true solution nearby. The approximate solutions used in this process are usually determined with purely numerical methods. The existence of true solutions is then obtained by solving a fixed point equation, using the contraction mapping principle in a ball centered at the approximate solution.
The proofs are based on a discretization of the problem, carried out and controlled with the aid of a computer. They involve a systematic reduction of the desired bounds to a finite number of trivial inequalities between (representable) real numbers. This is made possible by the fact that the maps are compact.
The general approach is quite standard by now. We start by associating to a functional space X an appropriate collection std(X) of subsets of X. A “bound” on an element u ∈ X is then a set U ∈ std(X) containing u, while a bound on a map g : X → Y is a map G : DG → std(Y), with domain DG ⊂ std(X), such that g(u) ∈ G(U) whenever u ∈ U ∈ DG . Notice that the composition of two bounds, if defined, is a bound on the corresponding composed map. This and other properties allow us to combine bounds on elementary maps into bounds on more complex maps, and thus to mechanize the necessary estimates.