An introduction to computer-assisted proofs for nonlinear equations: how to turn a numerical simulation into a theorem (Maxime Breden, École Polytechnique)

The goal of a posteriori validation methods is to get a quantitative and
rigorous description of some specific solutions of nonlinear ODEs or PDEs,
based on numerical simulations. The general strategy consists in combining
a priori and a posteriori error estimates, interval arithmetic, and a fixed
point theorem applied to a quasi-Newton operator. Starting from a nu-
merically computed approximate solution, one can then prove the existence
of a true solution in a small and explicit neighborhood of the numerical
approximation.
I will first present the main ideas behind these techniques on a simple
example, then describe a rather general framework in which they can be
applied, and finally discuss some applications in population dynamics and
fluid dynamics.