1. Introduction & Purpose

Nonlinear differential equations are essential to modern science. As these models have grown in complexity, numerical simulations have become indispensable tools for their analysis, particularly for systems in infinite-dimensional function spaces, such as those governed by partial differential equations. However, despite their importance, numerical methods come with inherent limitations. Approximations – whether from rounding errors or discretization – introduce uncertainties, and often without offering a posteriori error bounds. These limitations raise critical questions about the reliability of numerical results, particularly in chaotic systems, where even minor computational inaccuracies can lead to drastically different outcomes. The need for more rigorous, mathematically grounded computational techniques has never been more pressing in the pursuit of understanding these complex systems.

In response to these challenges, computer-assisted proofs have emerged as a compelling approach, blending traditional analysis and computational methods. In recent years, such techniques have seen increasing success, with notable examples including the proof of Jones’ conjecture [1], the proof of finite time blow-up for the compressible Euler and Navier-Stokes equations [2] and the proof of Marchal’s conjecture [3]. For further context, see the survey articles [4, 5].

Reference

[1]. J. Jaquette. A proof of Jones’ conjecture. Journal of Differential Equations, 266(6):3818-3859, 2019.

[2]. G. Cao-Labora, J. Gomez-Serrano, J. Shi, and G. Staffilani. Non-radial implosion for compressible Euler and Navier-Stokes in T3 and R3. ArXiv, 2023.

[3]. R. Calleja, C. Garcia-Azpeitia, O. Henot, J.-P. Lessard, and J. D. Mireles James. From the Lagrange triangle to the figure eight choreography: proof of Marchal’s conjecture. ArXiv, 2024.

[4]. J. Gomez-Serrano. Computer-assisted proofs in PDE: a survey. SeMA Journal, 76:459-484, 2019.

[5]. J. B. van den Berg and J.-P. Lessard. Rigorous numerics in dynamics. Notices of the American Mathematical Society, 62(9), 2015.

2. Outline & Descriptions

The objective of the tutorial Computer-Assisted Proofs in Nonlinear Analysis is to introduce participants to fundamental concepts of a posteriori validation techniques. This mini-course will cover topics ranging from finite-dimensional problems, such as finding periodic orbits of maps, to infinite-dimensional problems, including solving the Cauchy problem and proving the existence of periodic orbits.

For this tutorial, the proposed structure is as follows:

Day 1 (November 5th)
Morning Session (9am to 11am): Finite-dimensional problems (Module 1)
Introduction to the contraction mapping theorem and the Newton-Kantorovich approach. A brief overview of interval arithmetic will also be provided.

Afternoon Session (2pm to 4pm): algebraic equations (Module 2)
We will address the first class of infinite-dimensional problems by rigorously computing an inverse function using Taylor series and determining the square root of a periodic function via Fourier series.

Day 2 (November 6th)
Morning Session (9am to 11am): Taylor integration and periodic orbits (Modules 3)
We will focus on solving initial value problems for ODEs using Taylor series. However, depending on participants’ interests, we may spend more time studying periodic solutions to ODEs and PDEs.

Afternoon Session (2pm to 4pm): Interactive problem-solving and open discussion
We will have an open forum for participants to ask questions and explore more practical applications. We aim to share topics of research, fostering a collaborative exchange of ideas.

Each session will last 2 hours: 1 hour of theory followed by 1 hour of hands-on practical applications. The practical exercises will focus on implementing computer-assisted proofs using the Julia programming language.

3. Prerequisites

To support the programming aspect and enhance the learning experience, we will use the RadiiPolynomial software [6], an open-source tool I developed and published in 2021. Please bring your laptop to the tutorial!

A website has been setup where you will be able to find the lecture notes and exercises of the tutorial: https://olivierhnt.github.io/Computer-assisted-proofs-in-nonlinear-analysis/

Before coming to the tutorial, I highly recommend following the instructions at: https://olivierhnt.github.io/Computer-assisted-proofs-in-nonlinear-analysis/installation/

Reference

[6]. Olivier Henot. Radiipolynomial. https://github.com/OlivierHnt/RadiiPolynomial.jl, 2021. Software under MIT license.

4. Registration

https://forms.gle/igTCDRziSi77AEu56

5. Join us online

11/5

11/6