International Workshop on Validated Numerics for Computer-Assisted Proofs
Validated Numerics for Computer-Assisted Proofs
6-10 July 2026, ICMS, Bayes Centre, Edinburgh
Long Programme and Abstracts
Note: The programme is provisional and subject to changes.
Sun 05 Jul 2026
Arrivals and Check-in
Suggested activity
Mon 06 Jul 2026
09:00-10:00 Registration and refreshments
Join us at the ICMS, top floor of the Bayes Centre. Refreshments will be provided.
10:00-10:15 Housekeeping and Welcome
10:15-11:00 The beginnings of validated numerics, in memory of Hans Koch and Oscar Lanford
Jean-Pierre Eckmann - Université de Genève, Switzerland
Although “everybody” might know how this subject evolved, I will try to reconstruct how the early issues and difficulties came up, and how Koch and Lanford (and many others) worked to make this subject a common modern tool in analysis.
11:00-11:30 Coffee
11:30-12:00 Validated polynomial optimisation for computer-assisted proofs in ODEs
Jeremy Parker - University of Dundee, Scotland
I will present the sum-of-squares optimisation framework for finding polynomials which satisfy pointwise nonnegativity conditions. This can be used to construct certificates of different global properties and bounds in ODE dynamical systems whose vector field is a polynomial function. Specific examples are proving different definitions of global stability, and bounding global attractors, time averages, attractor dimension and orbit periods. Strong theorems govern when such methods can always give certificates, or give sharp bounds. CAPs can be constructed by validating the polynomial certificates using rational or interval arithmetic. If time allows I will describe how to adapt these methods to nonpolynomial, PDE and discrete-time systems.
12:00-12:30 Computer-assisted proof of existence and stability of solitary waves in the Whitham equation
Matthieu Cadiot - École Polytechnique, France
The Whitham equation is a nonlocal model used to study shallow water waves, capturing complex phenomena such as wave breaking, peaking, and various traveling wave solutions. In this talk, I will present a computer-assisted methodology for studying solitary waves—traveling waves that vanish at infinity. In particular, the method provides a framework for the constructive existence proof of a true solution in the close vicinity of an approximate, numerically computed solution. Furthermore, the tight control obtained over the solution enables us to enclose the spectrum of the linearization at the solitary wave, leading to a rigorous and conclusive stability analysis.
12:30-14:00 Lunch
14:00-14:45 Computer-assisted proofs in nonlinear dynamics based on spectral methods
Jan Bouwe van den Berg - Vrije Universiteit Amsterdam, Netherlands
Finding solutions of problems in nonlinear dynamics often involves simulations. Turning these numerical computations into mathematical theorems requires computer assistance. Such computer-assisted proofs focus on specific solutions (or invariant objects more generally) to specific equations. Nevertheless, in this talk we take a more universal viewpoint and describe a relatively simple spectral framework in which many of these problems can be cast. In particular, since these systems and their solutions are often locally analytic, one can recast the problem into one concerning sequence spaces of rapidly decaying coefficients, say of a Taylor, Fourier, or Chebyshev series. The core of the analysis is then to manipulate such sequences, e.g., evaluating derivatives and nonlinearities, by computer, while keeping track of truncation and rounding errors. We discuss how one can use basic complex and Fourier analysis to accomplish this task for a wide variety of problems in nonlinear dynamics.
14:45-15:30 Rigorous enclosure of Lyapunov exponents of stochastic flows
Hugo Chu - École Polytechnique, France
Rigorously enclosing Lyapunov exponents of stochastic flows is a long-standing and notoriously difficult problem: even determining the sign of the top exponent is often out of reach outside special structures or perturbative regimes. In this paper, we develop a computer-assisted method to obtain rigorous upper and lower bounds on Lyapunov exponents of stochastic flows under mild hypoellipticity assumptions. Our approach starts from the Furstenberg-Khasminskii representation of the top Lyapunov exponent as an ergodic average over the invariant measure of the associated projective process, but crucially avoids any rigorous computation of that invariant measure. Instead, we introduce a numerical adjoint method, amenable to rigorous numerics, and show that an approximate solution of the associated Poisson equation yields a certified enclosure of the Lyapunov exponent via an explicit bound on the residual. This converts a non-rigorous numerical approximation into a rigorous quantitative estimate. The method applies to systems on both compact and non-compact state spaces, does not require special geometric structure, and is not restricted to small-noise or other perturbative settings. We use it to prove positivity of the top Lyapunov exponent for several stochastic systems, including examples exhibiting noise-induced chaos and parameter-dependent sign changes, and we combine it with continuation methods to obtain rigorous bounds over large parameter regions.
15:30-16:00 Coffee
16:00-17:00 Discussions 1
Discussion Chair1
Outline topics: Open Problems, the scope of VN across Mathematics
17:00-18:00 Welcome Reception
Tue 07 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:30 Verified error bounds for sparse systems
Siegfried Rump - Hamburg University of Technology, Germany
The solution of sparse systems is ubiquitous in numerical computations. Despite several efforts, there were no satisfactory method for computing verified bounds for the solution and was one of the “Grand Challenges” in verification methods for decades. In this talk we present two algorithms to compute entrywise error bounds for the solution of general real or complex sparse systems with condition number up to the limit $10^{16}$. Our algorithms split into three subalgorithms for symmetric positive definite, symmetric indefinite and general input matrix $A$. A key point is a factorization of $A$ into $L_1L_2$ such that $L_1$ and $L_2$ have identical sets of singular values with the smallest one close to $\sigma_{\mathrm{min}}(A)^{1/2}$. A mathematically correct lower bound on $\sigma_{\mathrm{min}}(L_1) = \sigma_{\mathrm{min}}(L_2)$ is then computed using $L_1^T L_1$. Based on that a second method exploring the inertia of a symmetric/Hermitian matrix is presented. It is often slower but more robust, i.e., it may produce verified inclusions where the first method fails. We show how to compute inclusions with almost maximal accuracy for all entries, i.e., all bounds differ by few bits. That is based on a fast method to compute accurate approximations and bounds for extremely ill-conditioned dot products with a very efficient Matlab implementation. Both approaches are used to compute verified error bounds for the solution of least squares problems and for underdetermined linear systems. Inclusions of the solution of general real or complex systems of nonlinear equations with sparse Jacobi matrix are computed by transforming the problem into a linear system with point matrix and interval right hand side. All algorithms are implemented in pure Matlab/Octave and included from Version 14 of INTLAB, the Matlab/Octave toolbox for verified computations.
10:30-11:00 Root certification using disk arithmetic
Nicolae Mihalache-Ciurdea - Univ Paris-Est Creteil, France
Splitting algorithms provide a list of all the roots of a polynomial, however, most numerical implementations lack the proper framework to provide certification, i.e. a computer-assisted proof that the list is correct. In a work with François Vigneron, we address this issue, regardless of the underlying splitting algorithm, with minimal computational overhead. To ensure a strict control of the computational errors that is robust enough to withstand intensive iterations, we revisit and extend the theory of disk arithmetic. I will explain a simple algorithm based on two results, one regarding the localization of roots and one regarding the convergence of numerical refinements using Newton’s method.
11:00-11:30 Coffee
11:30-12:00 Existence of cycles of the doubling operator for coupled maps
Zainab Rahman - University of Portsmouth, England
We study two-dimensional non-invertible maps with multiple parameters, with critical points arising from a fold singularity. Working in spaces of pairs of analytic maps, we prove the existence of a two-cycle conjectured by Kuznetsov et. al. of the renormalisation (doubling) operator for systems with C-type critical scaling. We bound the universal constants that describe state-space scaling. Our work generalises the recent work on FS-type and FQ-type systems from fixed points to periodic orbits of the corresponding renormalisation operators. The proof relies on rigorous (validated) computations to establish that a variant of Newton’s method for the two-cycle is a contraction map. This is joint work with Andrew Burbanks and Maria Pickett.
12:00-12:30 A computer-assisted proof of dynamo growth in the stretch-fold-shear map
Benjamin Mestel - Open University (Retired), England
(Pending - On behalf of Farhana Pramy)
12:30-14:00 Lunch
14:00-14:45 On attractors of Fibonacci maps
Artem Dudko - Institute of Mathematics of the Polish Academy of Sciences (IM PAN), Poland
In 1990s Bruin, Keller, Nowicki, and van Strien showed that smooth unimodal maps with Fibonacci combinatorics and sufficiently high degree of a critical point have a wild attractor, i.e. their metric and topological attractors do not coincide. However, until recently there were no reasonable estimates on the degree of the critical point needed. In the talk I will present a constructive approach for studying attractors of maps, which are periodic points of a renormalization. Using this approach and rigorous computer estimates, we show that the Fibonacci map of degree d=3.8 does not have a wild attractor, but that for degree d=5.1 the wild attractor exists. The talk is based on a joint work with Denis Gaidashev.
14:45-15:15 (TBC)
Olivier Henot - National Taiwan University, Taiwan
(Pending)
15:15-15:30 (Motivation for discussion session. Chair: Ben Mestel)
15:30-16:00 Coffee
16:00-17:00 Discussions 2
Discussion Chair2
Outline topics: Common standards for frameworks, possible uses for AI and proof assistants.
17:00-18:00 Reception & Networking
Wed 08 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:15 Computer assisted proofs for invariant manifolds and their use in connecting orbit problems
Jason Mireles-James - Florida Atlantic University, USA
This will be an introductory/overview talk about computer assisted existence proofs for connecting orbits in nonlinear dynamical systems. I’ll give a quick review of some history, and describe some projected boundary value problems used to study heteroclinic/homoclinic connections. Connecting orbits take an infinitely long time to accumulate on an invariant object like an equilibrium, periodic orbit, or torus, and an important part of the argument is describing the orbit as time approaches infinity. One approach to this problem is to study the local stable/unstable manifolds attached to the invariant object, and the parameterization method of Cabre, de la Llave, Fontich, and Haro is a useful tool in this context. I’ll give a condensed overview of this topic as well, focusing on how to obtain higher order expansions equipped with validated error bounds. Then I’ll look at a few example applications and try to indicate some open problems/future directions.
10:15-11:00 Arnold Diffusion and Blenders in the Three-Body Problem
Maciej Capinski - AGH University Kraków, Poland
We present a computer-assisted methodology based on the propagation of topological discs and its use in analysis of global dynamics. The method combines topological techniques with validated numerics and can be applied to detect both diffusion as well as persistence of symbolic dynamics. We discuss its applications to Arnold diffusion and blenders in celestial mechanics.
11:00-11:30 Coffee
11:30-12:00 Computer Assisted Proofs for Nonlinear Problems in the Borel Plane and Validated Numerics for Complex Convolutions
Juan Miranda - Florida Atlantic University, USA
The Borel transform is a useful tool for studying functional equations whose solutions are infinitely differentiable but not analytic. For nonlinear problems, matters are complicated by the fact that the transform takes pointwise multiplications to complex convolutions. Nevertheless, Bonckaert and Maesschalck (2008) have shown that complex convolution results in a Banach algebra structure, after introduction of an appropriate norm. I will discuss how these tools are used to approximate non-analytic functions and obtain rigorous computer assisted error bounds on divergent series in computer assisted proofs.
12:00-12:30 Taylor models in Julia
Luis Benet - Universidad Nacional Autónoma de México (UNAM), Mexico
Abstract: In this talk, I present progress in the development of the package TaylorModels.jl which is written in Julia. First, I shall describe my own motivations (as a physicist!) to engage in this task. I will then discuss the generalities of the Taylor models, based in the work of M. Berz and K. Makino, and of M. Joldes. I will illustrate the use of our package in a short “live code” session. I will finish with some challenges we have with our package, looking forward for advices and tips.
12:30-14:00 Packed Lunch
14:00-18:00 HALF DAY SUGGESTIONS:
Wednesday has been planned as a half-day at the ICMS to provide participants with opportunities to network and explore the historic city of Edinburgh together in the afternoon. A number of activities are suggested and some will be led by the organisers.
(A) 15:00 Tour of the James Clerk Maxwell House, 14 India Street
David Kerridges - James Clerk Maxwell Foundation, Scotland
A tour has been arranged, with tour guide(s) from the James Clerk Maxwell Foundation, starting at 15:00 at 14 India Street, for those interested.
(B) Walk to Arthur’s Seat
A walk, with one of the organisers, to the top of Arthur’s Seat, the extinct volcano that stands 800 feet over central Edinburgh, giving panoramic views over the city, the Firth of Forth, and distant hills.
(C) Walk exploring Old Town, Royal Mile, Dean Village
A walk, with one of the organisers, starting at the ICMS and taking-in some of the famous sites in Edinburgh including Greyfriar’s Churchyard, Edinburgh Castle and the Royal Mile, Princes Street and the Scott Monument, and down into the picturesque Dean Village and the Water of Leith.
(D) Scottish Museum
The National Museum of Scotland is located near the ICMS, and not far from the Royal Mile.
(TBC)
Thu 09 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:30 The CAPD library - a tool for validation in dynamical systems
Daniel Wilczak - Jagiellonian University in Kraków, Poland
The CAPD library [1,2] is a C++ library devoted to validated numerics for dynamical systems. It has been developed for over 30 years by a research team at the Jagiellonian University in Kraków, Poland. The library is mostly oriented towards continuous-time systems and implements rigorous integrators for ODEs, higher order variational equations [3,4], differential inclusions [5], and a class of dissipative PDEs [6]. In the talk I’m going to present the basic interface of the library, then give a few one-screen short yet not very trivial case studies. I will present an application of the library to prove the existence of a uniformly hyperbolic chaotic attractor in a 4D non-autonomous ODE [7]. References: [1] https://github.com/CAPDgroup/CAPD [2] T. Kapela, M. Mrozek, D. Wilczak, P. Zgliczyński. CAPD::DynSys: a flexible C++ toolbox for rigorous numerical analysis of dynamical systems. Commun Nonlinear Sci Numer Simul 2021;101:105578. [3] P. Zgliczyński, $C^1$-Lohner algorithm, Found. Comp. Math, 2(4), pp.429-465 [4] D. Wilczak, P. Zgliczyński, $C^r$-Lohner algorithm, Schedae Informaticae 20, 9-46, 2011. [5] T. Kapela, P. Zgliczyński, A Lohner-type algorithm for control systems and ordinary differential inclusions, Disc. Cont. Dyn. Sys-B, 11(2), pp.365-385 [6] D. Wilczak, P. Zgliczyński. A geometric method for infinite-dimensional chaos: Symbolic dynamics for the Kuramoto-Sivashinsky PDE on the line. J Differential Equations 2020;269(10):8509–48 [7] D. Wilczak, Uniformly hyperbolic attractor of the Smale-Williams type for a Poincaré map in the Kuznetsov system, SIADS. 9 (2010), 1263-1283.
10:30-11:00 Rigorous integration of differential inclusions and delay differential equations in the CAPD library
Tomasz Kapela - Jagiellonian University in Kraków, Poland
(Pending)
11:00-11:30 Coffee
11:30-12:00 (Part I - TBC)
Polina Vytnova - University of Surrey, England
(Pending)
12:00-12:30 (Part II - TBC)
Caroline Wormell - The University of Sydney, Australia
(Pending)
12:30-14:00 Lunch
14:00-14:45 Rigorous integration of dissipative PDEs on the torus
Piotr Zgliczynski - Jagiellonian University in Kraków, Poland
We will describe the proof of the existence of symbolic dynamics for the Kuramoto-Sivashinsky PDE on the line: a semiconjugacy with the Bernoulli shift, the existence of countably many periodic orbits and homo- and heteroclinic connections between them. On this example of computer assisted proof we would like to explain how to perform rigorous numerics for dissipative PDEs with periodic boundary conditions and how to use finite dimensional tools from dynamics in the context of dissipative PDEs.
14:45-15:30 Lower bounds on the Hausdorff dimension of some Julia sets
Igors Gorbovickis - Constructor University, Germany
We present an algorithm for a rigorous computation of lower bounds on the Hausdorff dimensions of Julia sets for a wide class of holomorphic maps. We apply this algorithm to obtain lower bounds on the Hausdorff dimension of the Julia sets of some infinitely renormalizable real quadratic polynomials, including the Feigenbaum period doubling polynomial. This is joint work with Artem Dudko and Warwick Tucker.
15:30-16:00 Coffee
16:00-17:00 Discussions 3
Discussion Chair3
Outline topics: The Future, possibility for a Special Interest Group, VNCAP2028?
(TBC)
Fri 10 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:15 Computer-assisted proofs for periodic solutions in state-dependent delay equations
Jean-Philippe Lessard - McGill University, Canada
State-dependent delay equations (SDDEs) pose significant theoretical and computational challenges, as the delay depends on the evolving state through nonlinear composition terms. In contrast with ODEs, parabolic PDEs, or delay equations with constant delays, SDDEs may fail to generate a semiflow. Even when a semiflow exists, the dynamics evolve on an infinite-dimensional phase space, with the composition operator introducing additional analytical difficulties. As a result, periodic solutions, which are central to understanding recurrent dynamics, are particularly challenging to study in this setting. In this talk, we present a computer-assisted, constructive method to prove the existence of periodic solutions in genuinely state-dependent delay equations, without relying on perturbative reductions to ODEs or PDEs. Our approach combines Fourier expansions with a Newton–Kantorovich argument in a low-regularity Banach space. The nonlinear composition terms are handled rigorously using discrete Fourier transforms, contour integrals, and the discrete Poisson formula. We illustrate the method through three applications of increasing complexity: (1) a forced SDDE with prescribed period; (2) an autonomous SDDE where the period is part of the unknowns, following Calleja, Humphries, and Krauskopf (2018); and (3) an SDDE with a threshold nonlinearity, requiring unfolding parameters to handle the discontinuity and determine the period, based on Gedeon, Humphries, Mackey, Walther, and Wang (2025). This is joint work with Jan Bouwe van den Berg (VU University Amsterdam), Maxime Breden (École Polytechnique), Matthieu Cadiot (École Polytechnique), and Kevin Church (CRM, Montréal).
10:15-11:00 Rigorous computation of renormalization fixed points using Chebyshev series
Maxime Breden - École Polytechnique, France
In this talk, we revisit the computer-assisted study of renormalization fixed points initiated by Lanford, in his proof of the Feigenbaum conjectures related to period doubling cascades in families of unimodal maps. Our approach follows rather closely the original works in this field, the main difference being that we use Chebyshev series expansions instead of Taylor series. This generates some technical hurdles that I will discuss, but also makes the proof more general and versatile. In particular, we are able to get tight enclosures of Feigenbaum-like constants for other bifurcation cascades (e.g., period tripling), and for critical points of higher order. This is joint work with Jorge Gonzalez and Jason Mireles James.
11:00-11:30 Coffee
11:30-12:00 (TBC)
(TBC)