GitHub

Week 10 Lecture 1: Computer-assisted proofs in practice

Last week we finished the second phase of the course, Introduction to computer-assisted proofs. We will now move into the third, and final, phase of the course, Computer-assisted proofs in practice.

During this phase we will look at existing papers in analysis that make use of computer-assisted proofs. The goal is both to see examples of how a mathematical problem can be reduced to a rigorous computation, and to see new examples of algorithms in rigorous numerics.

For this lecture, we will look at some categories of papers and methods and discuss which of them we are interested in diving deeper into.

Remark

Most of the papers discussed below are either my own or a selection of papers that I'm somewhat familiar with.

Spectral geometry

We are here interested in how eigenvalues of the Laplacian, i.e. solutions to $\Delta u = \lambda u$, depend on the domain.

My papers:

Others:

The papers all make use of the Method of Particular Solutions (MPS) for approximating the eigenfunctions. Error bounds are computed by controlling the approximation on the boundary of the domains. Some of them also make use of rigorous finite element methods (FEM) for computing indices of the eigenvalues. The paper Monotonicity of the first Dirichlet eigenvalue of regular polygons also has a lot of asymptotic computations.

Cusped waves

My papers:

The papers make use of spectral methods for computing approximate solutions. The rigorous verification is then done using a fixed point argument. For the fractional KdV equation a significant amount of work is required to handle the singular endpoints.

Self-similar blowup

My papers:

The existence of the self-similar solutions is proved using a combination of a rigorous ODE solver and asymptotic analysis at infinity.

Methodological papers

The paper discusses an approach for solving differential equations using spectral methods. The radii polynomial approach is a structured way to set up the fixed point problem around the approximate solution.

They describe a constructive version of the implicit function theorem and use this to study branches of solutions.

Longer papers