In the past decade, rigorously verified computing has primarily been applied to a range of ordinary differential equations. We are witnessing the emergence of the field of computational proofs for infinite dimensional nonlinear dynamics generated by partial differential equations, integral equations, delay equations, and infinite dimensional maps.

Some early successful applications of these methods for infinite dimensional problems have been: partially resolving a long-standing conjecture for Wright's delay equation; proving spatio-temporal behaviour in the Kuramoto-Sivashinsky PDE; finding 2D and 3D steady states in the Ohta-Kawasaki model for di-block co-polymers; and proving spontaneous periodic orbits in the Navier-Stokes flow. But this is just a beginning. To set the scene for the future, two open problems on the horizon are:

1. Connecting orbits in the Navier-Stokes equation for fluids. Recently, numerical evidence has been found for trajectories in the Navier-Stokes equations (with suitably chosen boundary conditions) that are homoclinic to periodic orbits. If we can rigorously validate the existence of such orbits, this would imply, through forcing results, the first mathematically rigorous proof of chaotic flow in fluids (as described by the Navier-Stokes equations in 3D).
2. Connecting orbits in ill-posed PDEs. Ill-posed PDEs (with no suitable initial value problem) that come with a variational structure allow for the construction of a Floer homology. Connecting orbits are essential ingredients of this construction. If we can rigorously compute such connecting orbits, they yield specific “local” information, which when combined with generic global analytic arguments, will lead to powerful forcing results. Early steps towards this long-term goal are starting to appear.

Both of these problems highlight that the interplay, through forcing theorems, of global analysis and local rigorous computations, can lead to very powerful results in infinite dimensional dynamical systems. Moreover, since the dynamics are highly nonlinear, a computer-assisted approach seems the only way forward in these types of problems.

The aim of the workshop is to foster collaboration in order to develop a flexible analytic strategy tied with corresponding fast and robust algorithms. The combination of qualitative global analysis with quantitative information from rigorously verified computations will provide novel insights in the dynamics of the infinite dimensional systems that model pattern formation, biological networks, fluid flows, etc.