Logo

International Workshop on Validated Numerics for Computer-Assisted Proofs

Validated Numerics for Computer-Assisted Proofs

6-10 July 2026, ICMS, Bayes Centre, Edinburgh

Notes from focussed discussion sessions

Monday, Discussion 1: Open Problems Session

Chairs: Mark Pollicott and Julia Slipantschuk

On Monday afternoon, we hosted an informal Open Problem session. In advance of the session, we encouraged all participants to bring unsolved problems, preliminary results, or grand ideas to the floor, with an assurance that no polished presentations would be required (a quick blackboard sketch - a single slide’s worth - or just a few minutes of explanation would be enough). We also invited any anecdotes from the participants’ experiences with computer-assisted proofs. Participants could provide these in advance via email, or during the session itself.

Some of the problem areas discussed, and questions posed, are summarised below.

1 Julia Sets

The family of degree 2 polynomial maps $T:\mathbb{C}\to\mathbb{C}$ of the complex plane have associated their Julia sets \begin{equation} J = \overline{\left\lbrace z\in\mathbb{C}: T^n(z)=z,\ |(T(z))'|>1\right\rbrace}. \end{equation} (i.e., the closure of the repelling periodic points). One can then associate each Julia set $J$ the value of its Hausdorff dimension $\mathrm{dim}_H(J)\in[0, 2]$. Of particular interest is the case of quadratic maps $z\mapsto z^2 + c$.

Let $c_F = −1.401155189\ldots$ be the Feigenbaum parameter, i.e., the limit of the period doubling bifurcation values along the real axis, starting from the main cardioid of the Mandelbrot set. In [2] it was shown rigorously that the Hausdorff dimension of this Julia set $J_{c_F}$ satisfies \begin{equation} 1.49781 \le \mathrm{dim}_H \left(J_{c_F}\right) < 2. \end{equation} Furthermore, they show that for any $c_F < c < −3/4$ there is a lower bound $\mathrm{dim}_H(J_c) > 4/3$.

Question. Are there good upper bounds on these dimensions?

The lower bounds come from the approach of McMullen [4] based on Markov Partitions and matrices. An upper bound would need to use an infinite iterated function scheme (through inducing).

By way of context, it is known that $[c_F,1/4]\ni c \mapsto\mathrm{dim}_H(J_c)$ is continuous (by work of McMullen) and real analytic on hyperbolic components (by work of Ruelle). Combining the lower bounds on the dimension with work of Jaksztas and Zinsmeister [3] it follows that $[c_F , −3/4]\ni c \mapsto \mathrm{dim}_H(J_c)$ is $C^1$.

(Artem Dudko: Considering the Hausdorff dimension and measures for Julia sets of maps that are renormalisation group fixed points. Questions regarding the likely true value prompted by recent bounds. What do we know about the dynamics on the attractor? (We can rescale rather than iterate due to RG equations.))

2 Central configurations and n-bodies

We can consider the dynamics of $n$ masses $m_i$ $(i = 1,\ldots,n)$. These are assumed to interact by gravitation whereby the gravitational acceleration vector produced on each mass by all the others should point toward the centre of mass and be proportional to the distance to the centre of mass. After some simplifications the equations in $\mathbb{R}^3$ can be reduced to \begin{equation} −\lambda q_i = \sum_{j\neq i}\frac{m_i(q_j − q_i)}{|q_j − q_i|^3}\quad\mbox{where $i=1,\ldots,n$,} \end{equation} for some constant $\lambda$ [5].

For a finite set of $n$ masses one can ask how many possible configurations there are.

For $n = 3$ the finiteness and classification of the solutions has been known for centuries . The (three) collinear configurations were discovered by Euler in 1767. In 1772 Lagrange showed that there is only one non-collinear configuration, which corresponds to the vertices of an equilateral triangle.

For $n = 4$ it was shown by Moeckel-Hampton [6] in 2005 that there are finitely many configurations, and this number lies between 32 and 8472. Their proof was computer assisted.

For $n = 5$ it was shown by Albouy and Kaloshin [1] that for almost all choices of masses (the exceptional cases corresponding to when the $5$-tuple of positive masses satisfies two given polynomial conditions) then there are finitely many solutions.

However, for $n > 5$ nothing appears to be known.

Question. In dimensions $n > 5$ are there only finitely many configurations?

(Piotr Zgliczynski: How can we determine the numbers (or numbers of types) of configurations that are central, what symmetries exist, how do the configurations fall into classes? How to search the space, ruling-out regions with no configurations, while avoiding dealing with / resolving all bifurcations? Lyapunov-Schmidt reduction.)

3 Topological entropy

Let $f:\mathbb{R}^2\to\mathbb{R}^2$ be the Henon transformation defined by \begin{equation} f(x, y) = (1 − ax^2 + y, bx), \end{equation} with the original values $a = 1.4$ and $b = 0.3$. Let $\Lambda\subset\mathbb{R}^2$ be the associated invariant set.

Given $n\in\mathbb{N}$ and $\varepsilon >0$ we let $N(n, \varepsilon)$ be smallest number of $(n, \varepsilon)$-balls \begin{equation} B(y, \varepsilon) = \bigcap_{k=0}^{n-1}f^{−k}B(f^ky, \varepsilon), \end{equation} needed to cover $\Lambda$ and then denote \begin{equation} h(n, \varepsilon) := (1/n) \log N(n, \varepsilon). \end{equation} The topological entropy $h(f)$ takes the value \begin{equation} h(f) = \lim_{\varepsilon\to 0}\limsup_{n\to\infty} h(n, \varepsilon). \end{equation}

Question. What is the value of the topological entropy of f? Find precise numerical bounds.

There are lower bounds coming for the entropy of generalized Smale horseshoes for which the associated invariant cantor set is contained in $\Lambda$.

From the work of Yomdin [7] and Newhouse there are estimates on this convergence. In particular, there exists $c > 0$ and such that the difference between $h(f)$ and $h(n, \varepsilon)$ is bounded by \begin{equation} c\frac{\log | \log \varepsilon|}{| \log \varepsilon|}. \end{equation} This leads to upper bounds on $h(f)$ which Newhouse had numerical estimates on.

(Daniel Wilczak: bounding topological entropy (+Piotr Zgliczynski) for Poincare maps.)

4 Hyperbolicity of Julia sets

The Mandelbrot set $\mathbb{M}\subset\mathbb{C}$ consists of those complex values $c$ for $T_c(z) = z^2 + c$ for which the associated orbit ${T^n_c(0)}_{n=0}^\infty$ is bounded. We can associate to $c\in\mathbb{M}$ the Julia set \begin{equation} J_c = \overline{\left\lbrace z\in\mathbb{C} : T^n(z) = z,\ \lvert(T(z))'\rvert>1\right\rbrace}. \end{equation} We say that the Julia set $J_c$ is hyperbolic if for any $z \in J_c$ we have that $|T′_c(z)| > 1$.

For example, all points $c$ in the interior of the main cardioid give rise to hyperbolic points. It is conjectured that those $c$ for which the Julia set is hyperbolic are dense in $\mathbb{M}$ (which would imply that the Mandelbrot set is locally connected).

Question. For a given value $c\in\mathbb{M}$ can one determine if $J_c$ is hyperbolic? In particular, if $c = −3/2$ can we know if $J_c$ is hyperbolic?

(Nicolae Mihalache: Considering the Mandelbrot set and previous questions posed by Milnor. Is (for example) -1.5 in a hyperbolic component of the Mandelbrot set? What would be a good approach to tackle this problem, given the clustering of hyperbolic components?)

5 Application to Hilbert’s 16th problem (polynomial flows in the plane)

6 Finding Lyapunov functions

7 Automatic solutions to Engineering problems

8 Matrix norms

Siegfried Rump (in Session 3):

Question. Can we estimate efficiently $\lVert A^{-1}\rVert_{\infty}$ for finite matrices, given bounds on $\lVert A^{-1} \rVert_{2}$?

References

Tuesday, Discussion 2: Standards, Tools

Chair: Ben Mestel

1. Standards for Validated Numerics for Computer-Assisted Proofs.

Overall the group was somewhat skeptical of standards, at least if adhered to too rigorously. The basic IEEE standard for floating-point arithmetic introduced in the 1980s had been great success and was supported by the group, enabling researchers in validated numerics to be sure of the rounding errors in floating point calculations.

However, it was generally felt that the subsequent IEEE standards for interval arithmetic (both the original standard - no longer in force - and the simplified version) had not been so successful. It was pointed out that precise implementation of the standard for infinite intervals led to mathematically nonsensical results. Workshop participants who were involved in the authoring and maintenance of interval-arithmetic packages reported that they did not implement the interval standard in totality, but instead implemented a subset of the standard which they knew would yield mathematically correct results.

Several speakers agreed that there are unhelpful features in the interval arithmetic standard (examples included how infinite intervals are handled and whether certain intervals test as empty or not) which had led groups to avoid impemeting those particular parts. Standard 1788 was not followed strictly due to these (and other) pathological cases. The group also noted that there is sometimes a tradeoff between adhering strictly to standards vs speed. The consensus was that standards covering rigorous numerical functional structures might not be helpful, unless these were minimal to avoid considerations like those above, and certainly not if built on top of the existing IEEE standard for interval arithmetic.

However, it was felt that it would be useful to build a suite of standard test examples so that different systems/implementations could be tested for correctness and performance. There was a much more positive response to this idea of sharing unit tests and functional tests for all of our libraries, where possible in a language-agnostic way. We also discussed the Sage-math idea of combining lots of tools into a collection with a common interface language, which would require writing wrappers for individual tools. This wasn’t universally thought to be a useful idea.

It was pointed out that practitioners of VNCAP should regularly check the accuracy of their own computers, not least because errors had been found in the past, most notably in the Pentium processor.

The idea of building a suite of standard test examples or benchmark problems, with a particular emphasis on correctness rather than necessarily speed, was very well-received. The point was made that the construction of the suite should potentially be handled with care or be varied and large, and that speed should not be the primary consideration, given that a limited benchmarking suite could cause optimisation/tailoring specifically to only these tests/examples rather than general efficiency.

We spent some time discussing the difficulties in communicating validated objects, and numerical objects generally, between different software implementations and frameworks, and between different groups of researchers, sometimes creating a barrier to collaboration, with this becoming even more acute for multiple precision objects and differing binary layouts.

The issue of blackbox software led to an interesting discussion, with the (perhaps counterintuitive) observation that widespread use of backbox software can actually increase the visibility of bugs and therefore lead to them being fixed.

2. The use of AI in the VNCAP field.

Participants stressed that while in certain circumstances AI tools such as Anthropic’s Claude, Alphabet’s Gemini and Open AI’s ChatGPT (amongst others available systems) might be used as a tool, the current state of generative AI and Large Language Models, although much improved since the early versions, was such that they could not be relied upon for rigorous mathematical work. Certainly, any software/code written by these package required careful checking by humans and, likewise, any mathematical results needed to be checked carefully. It was noted that the code produced was sometimes not up to date and would not run on the latest versions of computer languages, partly a result of the rapid evolution of new languages such as Julia.

It was thought that generative AI might be most helpful in the verification and debugging of human-produced code, where weaknesses and errors highlighted by the generative AI tool might be checked by the code-writers thereby possibly saving considerable time expended on debugging programs (provided that the rate of false-positives for detecting errors is not too high). It was noted that there had been many bugs found in the original code for the famous Appel-Haken proof of the Four Colour Theorem.

It was suggested that while a bespoke AI for VNCAP was probably not worthwhile or feasible, it might be useful to produce one or more specific CAP prompts (pointing to documentation, containing examples, etc) for debugging. It was also suggested that this should still be done in conjunction with a general (non-CAP prompted) check in order to avoid bias. We discussed the possibility of a “CAPify context” for LLMS: the idea is that a corpus of existing work and/or prompts that include common desired features of CAPs could be pre-pended to LLM prompts, in order to set-up the right context for existing commercially-developed LLMS. This was a more reasonable idea than attempting to train a custom CAP-LLM (which would take enormous resources). A drawback of setting context was that this might introduce unhelpful biasing. It would be useful to experiment with these issues.

3. Automatic Theorem Proving.

There was some discussion of the possibility of automatic theorem proving (ATP) (and indeed some packages had advanced verification options that came close to this goal). It was generally felt that we were still far away from ATP in the VNCAP, certainly of the kind that was been developed and popularised in pure mathematics.

4. Meeting adjourned for the Social and Networking session of the workshop

The discussion continued in small groups during the Social and Networking session and it was reported anecdotally that the discussion had continued very fruitfully during the session. Of particular note was that participants associated with various interval arithmetic packages, and researchers with their own bespoke solutions, had very helpful interactions, leading to agreements to share unit and functional tests. Indeed, a greater coordination between the interval-arithmetic groups might ultimately be the most useful outcome of Discussion Session 2.

Thursday, Discussions 3: Future Activity

Chair: Andrew Burbanks

(Siegfried Rump posed an open problem, added to the notes for session 1 above.)

1. Information exchange of activities planned in the next two years

Upcoming events:

a. XXVII International Workshop for Young Mathematicians “Dynamical systems”, September 20-26, 2026 School on dynamical systems in Krackow, Poland, 6 courses given by 6 speakers (3 of whom were at our workshop), 6 hours each, aimed at PhD students and others wanting to engage with the research area. Mostly on validation and topological dynamics. Travel costs plus a small fee are the barriers to engagement

b. 21st International Symposium on Scientific Computing, Computer Arithmetic, and Verified Numerical Computations (SCAN), Kitakyushu, Japan, September 13–17, 2027 (invitation only)

c. Computer-Assisted Proofs in Delayed and Infinite-Dimensional Dynamical Systems, week-long series of talks at International Centre for Mechanical Sciences (CISM) in Udine, Italy, May 3-7 2027 School to teach infinite dimensional techniques for PDEs, etc. 6 speakers for 1 week.

d. SIAM Conference on Applications of Dynamical Systems (DS27/Snowbird), May 23-27 2027, Atlanta, Georgia, USA. It was suggested that participants consider setting up a VNCAP mini-symposium.

e. Dynamics, Topology, and Computations, Bedlewo, Poland, every 3 years. Based on a princple of combining two broad topics each time, e.g., dyn sys and CAP. Good venue in forest, castle, nothing to do but maths and social. June. Next meeting in 2028. Low entry fee with many things included. 1 week.

2. Coordination of activities in the VNCAP area

We discussed the possibility of a Special Interest Group in CAP to coordinate activity and potentially advocate for our interests. What form could it take. How could it be organised. We discussed the possibilities of dedicated interval arithmetic hardware clusters, although agreed that these seemed unlikely.

The idea of the SIG didn’t seem to generate very much interest, but participants were keen on some sort of web site and mailing list that could be used to help keep the community informed of upcoming events, collect together links to common tools, libraries, and software, and other resources. The idea would be to start with something modest and extend it / grow it. CAP and dyn sys seemed a natural focus.

a. Formal SIG not favoured, given current time pressure on university staff.

b. Maintenance of a webpage would be helpful - possibly an extension of vncap.com with new title? But note: https://www.reliable-computing.org

c. Establishment and maintenance of an email list for information exchange.

d. Low probability that lobbying chip manufacturers for support for interval arithmetic/VNCAP would be successful, but that sharing details of computational resources and techniques is useful.

3. Future workshops/meetings

For future activity: how can we foster it? What kind of meetings are helpful? What didn’t / doesn’t work? How can we keep this dialogue going? Should we pass on the baton for VNCAP28? Or should we apply to run this format again at ICMS? What other conferences and opportunities are there to meet and work together? What format would be helpful?

Could we build a scientific case for an extended INI programme (1+ months residential)? This would require identifying perhaps 1-3 “big” problems or areas on which focussed work could yield a breakthrough. We would also need to identify which adjacent groups/disciplines should be invited in order to have a critical mass.

Perhaps more realistically in the shorter term, a more modest follow-up grant, research in pairs grant, or a repeat workshop in 2 years. Again, the host encouraged the group to think about which adjacent disciplines we should invite. There was the suggestion of the pattern formation community, in particular a group at Surrey.

a. Possible follow-up meeting/research in groups at the ICMS

b. Possible INI programme thought to be overambitious, but a VNCAP theme/workshop at a related meeting might be possible. One month programme might be more realistic.

4. Possible book from the meeting discussed and interested people were invited to email the VNCAP meeting organisers if interested in contributing.

A scientific publisher is interested in publishing an edited volume on the themes of the workshop. We have some participants interested already in contributing a chapter or short article. Is there any further interest? Possibly based on discussions had during this workshop. Participants were encouraged to get in touch.

The chair emphasised that expository aticles are also welcome, in particular for early chapters of the volume. This led to the idea of groups contributing small case studies: an interesting problem with challenges that lead naturally into CAP, with short specific examples of how CAP could be implemented. The idea would be that this should be suitable for PhD level readers, or those from more distant disciplines, in order to provide a route into the field. There seemed to be quite a lot of interest in this possibility and the chair agreed to follow-up with participants after the workshop. [It was noted that Daniel Wilczak had already published a paper with some examples of this form and we should take a look at the format, whether it could be adapted to form a template for contributions of case studies.]

Tagline:

Can you contribute a short case study, leading from an interesting problem quickly to CAP in an accessible way?

The chair noted that the organising committee woud be seeking feedback from all present.

Friday, Final Session: Closing Remarks

Chair: Andrew Burbanks

The chair thanked the ICMS for hosting the workshop and for administering, including thanks to Alex, Gillian, Jane, and the other ICMS staff.

The chair explained how ICMS workshops are funded and put together and thanked the sponsors: in particular, the workshop was supported by the ICMS via a Workshop Grant, the London Mathematical Society (LMS) via a Scheme 1 Conference Grant, and the Glasgow Mathematical Journal Trust. (ICMS is supported by the Engineering and Physical Sciences Research Council (EPSRC), Heriot Watt University, and the University of Edinburgh.)

We agreed to look into follow-up activities.

The chair extended a big thank you to participants for creating such a positive atmosphere and noted that the organisers are happy to put people back in touch with each other.

We agreed to put slides from talks onto the web site over the next week, and to approach participants again re potential book contributions including case studies that provide routes into CAP from adjacent discplines.

All participants were reminded to fill-in their expenses claims.

Finally, we encouraged everyone to submit their feedback and to copy to the chair any further comments. These will be especially helpful in improving future workshops and in making the case for a follow-up meeting.