International Workshop on Validated Numerics for Computer-Assisted Proofs
Validated Numerics for Computer-Assisted Proofs
6-10 July 2026, ICMS, Bayes Centre, Edinburgh
Abstracts and Slides
Click the presentation icon for each talk to access the slides. (Where slides were not used, we have attempted to capture some of the activity at the blackboard.)
Transcripts of discussion sessions are also available by clicking the notes icon.
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
Session 1. Chair: A Burbanks
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 Break
Session 2. Chair: A Burbanks
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
Session 3. Chair: B Mestel
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 Break
16:00-17:00 Discussions 1: Open Problems and Scope
Discussion Chairs 1: M Pollicott and J Slipantschuk
This session is a very informal opportunity for participants to tell the workshop about recent (possibly unpublished) results, work in progress, future plans/projects, blue-sky ideas for future applications and to discuss academic collaborations.
17:00-18:00 Welcome Reception
Tue 07 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
Session 1. Chair: A Burbanks
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 - 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 Break
Session 2. Chair: Julia Slipantschuk
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
Joint work with Farhana Framy (Open University) and Andrew Gilbert (Exeter). The Stretch-Fold-Shear (SFS) operator $S_\alpha$ is a functional linear operator acting on complex-valued functions of a real variable $x$ on some domain containing $[-1, 1]$ in $\mathbb{R}.$ It arises from a stylized model in kinematic dynamo theory where magnetic field growth corresponds to an eigenvalue of modulus greater than 1. When the shear parameter $\alpha$ is zero, the spectrum of $S_\alpha$ can be determined exactly, and the eigenfunctions corresponding to non-zero eigenvalues are related to the Bernoulli polynomials. The spectrum for $\alpha > 0$ has not been rigorously determined although the spectrum has been approximated numerically. In this talk, a computer-assisted proof is presented to provide rigorous bounds on the leading eigenvalue for $\alpha \in [0,5]$, showing inter alia that $S_\alpha$ has an eigenvalue of modulus greater than $1$ for all $\alpha$ satisfying $\pi/2 < \alpha \le 5$, thereby partially confirming an outstanding conjecture on the SFS operator.
12:30-14:00 Lunch
Session 3. Chair: J Slipantschuk
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 About the fate of the Rotating Eight families
Olivier Henot - National Taiwan University, Taiwan
(Pending)
15:15-15:30 (Motivation for discussion session. Chair: Ben Mestel)
15:30-16:00 Break
16:00-17:00 Discussions 2: Methodologies, languages, platforms, standards and AI / proof assistants
Discussion Chair 2: B Mestel
After a brief presentation before tea, the discussion session will focus on how best to harmonise work between research groups so that researchers can take advantage of all the different VNCAP environments with the easiest learning curve. We will also discuss whether it would useful to develop an an international standard building on IEEE 1788-2015 IEEE Standard for Interval Arithmetic (and its simplified version IEEE 1788.1-2017 IEEE Standard for Interval Arithmetic (Simplified)) and, of course, what is the future of AI and/or proof assistants in VNCAP.
17:00-18:00 Social & Networking
Wed 08 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
Session 1. Chair: A Burbanks
09:30-10:15 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.
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 Break
Session 2. Chair: J Slipantschuk
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
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 advice and tips.
12:30-13:30 Packed Lunch
Packed lunches will be made available to collect. Participants are welcome to either eat them at the ICMS, or take them away for afternoon activities.
13:30-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 possible activities are suggested below.
(A) Tour of the James Clerk Maxwell House, 14 India Street
David Kerridges - James Clerk Maxwell Foundation, Scotland
14:00 Leaving ICMS with Mark Pollicott, 15:00 Tour starts at 14 India Street
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. James Clerk Maxwell (1831-79) was born in this house at 14 India Street, Edinburgh. In 1993 the Foundation acquired Maxwell’s birthplace. This elegant Georgian house, after period restoration, displays a growing collection of heritage material associated with James Clerk Maxwell, his associates and family circle. [See Maps and Locations of Interest]
(B) Walk to Arthur’s Seat
14:30 Leaving JMCC with Ben Mestel
Possible activity suggestion: a walk 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. [See Maps and Locations of Interest] Disclaimer: Participants are advised that they should dress appropriately for the weather, wear suitable footwear, bring water and sun protection as needed, and take into account any medical conditions if deciding to undertake this walk. Participants take responsibility for undertaking the walk and are advised to reconsider if conditions are not suitable.
(C) Walk exploring Old Town, Royal Mile, Dean Village
13:00 Leaving ICMS with Andrew Burbanks
Possible activity suggestion: a walk, 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. [See Maps and Locations of Interest] Disclaimer: Participants are advised that they should dress appropriately for the weather, bring water and sun protection as needed, and take into account any medical conditions if deciding to undertake this walk. Participants take responsibility for undertaking the walk and are advised to reconsider if conditions are not suitable.
(D) Museums and Galleries
The National Museum of Scotland is located near the ICMS, and not far from the Royal Mile. Other venues of interest include the Writer’s Museum and the National Galleries of Scotland. Further afield, across the Water of Leith, is the National Galleries of Scotland: Modern One housing a modern art collection. [See Maps and Locations of Interest]
Thu 09 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
Session 1. Chair: A Burbanks
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
We describe a modification of the Lohner algorithm which allows us to effectively compute rigorous upper bounds for reachable sets of control systems, solutions of ordinary differential inclusions, perturbations of ODEs, and delay differential equations. Two different approaches to handling perturbations will be compared: the first based on component-wise estimates and the second using logarithmic norms. The implementation in the CAPD library merges these methods into one algorithm. Example solutions in CAPD syntax will be presented.
11:00-11:30 Break
Session 2. Chair: J Slipantschuk
11:30-12:00 Euler-Maclaurin Formula in Hausdorff dimension estimates
Polina Vytnova - University of Surrey, England
(Pending)
12:00-12:30 Euler–Maclaurin on a computer
Caroline Wormell - The University of Sydney, Australia
At times, we are called upon to sum an infinite series, that may decay quite slowly (e.g. polynomially). In many cases, the summands can be embedded in a complex analytic one-parameter family. This trick allows us to employ the Euler–Maclaurin formula to convert it into an asymptotic expansion involving an integral, various derivatives, and a remainder term. Practical implementation suggests a range of exciting and interlocking discretisation questions. In this talk, I will discuss one approach for doing this efficiently while maintaining one’s sanity. Some applications in parabolic dynamical systems will be considered.
12:30-14:00 Lunch
Session 3. Chair: C Wormell
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 Break
16:00-17:00 Discussions 3: Future activity
Discussion Chair 3: A Burbanks
The final discussion session is an opportunity for workshop participants to discuss future activity in the VNCAP research space. How can we foster future activity? Do we need a Special Interest Group to coordinate and advocate for the community and, if so, how might it be best organised? Would we benefit from future workshop conferences and, if so, what would work best? Would anyone like to follow-up with VNCAP2028? Are there further upcoming workshops and conferences that would be of interest? A scientific publisher is interested in a book on the themes of this workshop. We already have some interest in contributing chapters - who might be interested in joining?
Fri 10 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
Session 1. Chair: A Burbanks
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 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.
11:00-11:30 Break
11:30-12:00 Breakout discussions
We encourage participants to continue their discussions at the blackboards in the breakout areas.
12:00-12:30 Closing remarks and thanks
Session Chair: A Burbanks
We conclude the workshop with thanks to all involved in supporting, organising, and participating. We summarise the process for applying for and planning ICMS workshops and briefly discuss again the potential for follow-up activity.
12:30-14:00 Packed Lunch
Packed lunches will be provided, in order that participants can collect these if needing to leave promptly for onward travel, or can eat them at the ICMS.
14:00-14:00 Close
Participants are welcome to remain in the ICMS, but need to ensure that they leave the Bayes Centre promptly by 16:45, taking all possessions, ready for building closure.
Credit: Slideshow and Notes SVG Vector icons are from the collection Simple Line Vectors by Nishanth Kunder, released under CC Attribuion License.