Validated numerical proofs

Lecturer

Dr. Liam Hodgkinson, The University of Melbourne

Synopsis

Simulations and machine learning techniques are widely used to explore complex systems, yet they come with a critical limitation. Floating-point errors accumulate, chaotic trajectories diverge, and black-box models can produce plausible mirages without warning. Validated numerics restores mathematical certainty to computing by turning rough approximations into rigorous guarantees. While automated solvers can only suggest candidate answers, by providing error bounds, validated numerics can achieve what black-box algorithms cannot alone. This rigorous approach drives breakthroughs on some of the hardest problems in science today, from certifying chaos and critical behavior of models to the ongoing progress in verifying blow-up profiles in the unforced Navier-Stokes equations. In this course, you will learn how to bridge the gap between fast simulation and rigorous proof, making your computer’s output undeniable.

• Week 1 introduces the concept of rigorous computation, demonstrates several failure modes in naive approaches, and positions polynomials as a primary tool for exact computation.
• Week 2 covers the basic principles of interval arithmetic and applications for solving ordinary dif-ferential equations, specifically leveraging Taylor’s theorem.
• Week 3 transitions to the analytical verification of solutions, using fixed point theory and interval Newton methods to prove the existence and uniqueness of roots in nonlinear systems.
• Week 4 extends these rigorous techniques to global contexts, applying branch and bound for certi-fied global optimization and Galerkin methods for validating solutions to differential equations.

Course Overview

• Week 1: Foundations of Rigorous Computation
  • The inadequacy of standard computational approaches and the need for rigour
  • Introduction to validated numerical proofs and arbitrary precision (and the Arb software package)
  • Theoretical and practical advantages of working with polynomials; root counting methods
  • Chebyshev polynomial approximation
  • Problem Set 1: Observing failures of floating-point arithmetic in high-degree polynomials
• Week 2: Interval Arithmetic
  • Performing basic arithmetic with intervals; the Inclusion Property
  • Automatic differentiation and consequences of Taylor’s theorem for enclosures
  • Frobenius method for ODEs
  • Rigorous adaptive quadrature
  • Problem Set 2: Building interval-based Taylor model for ODEs
• Week 3: Linear and Nonlinear Systems
  • Fixed point theory (Banach, Brouwer, Schauder)
  • Matrix interval arithmetic (Oishi-Rump)
  • Interval Newton methods
  • Problem Set 3: Solving and verifying roots of linear and nonlinear systems
• Week 4: Global Solvers and Final Project
  • A posteriori error bounds
  • The branch and bound approach
  • Galerkin, kernel, and neural network approximations
  • Final Project: Use techniques developed so far to prove one of two results; either (i) existence of a solution to a nonlinear BVP, or proving the global minimum of a challenging function.

Prerequisites

Multivariable calculus, fundamentals in linear algebra, real analysis, metric spaces, some programming experience.

This is a foundational course, appropriate for all students at the Honours/Masters level with the appropriate prerequisites.

Assessment

• 3x Problem sets – 5% each (15% total)
• Project (35%)
• Final exam (50%)
  • If the classroom cohort is greater than 16 students, this will be a handwritten Invigilated exam (2hrs + 15 mins reading time)
  • If the classroom cohort is less than or equal to 16 students, this will be a 5 minute oral examination for each student

Resources/Pre-reading

There is no pre-reading required for this course.

Students are expected to bring their own laptops/devices to Summer School to complete this subject.

The coding part of the unit will be taught in the open source programming environment Python, using the library python-flint for arbitrary-precision ball arithmetic (which was previously distributed under the name Arb). To prepare for this material students should install Python 3.11 or later ( https://www.python.org/downloads/ ) on their own machine, and then run “pip install python-flint” (without the quotes) at a terminal.

To run Jupyter notebooks, you should also install VSCode ( https://code.visualstudio.com/ ) along with the extension for Jupyter (VSCode will automatically suggest this when you open a Jupyter notebook .ipynb file if you do not have the extension installed).

There is a short example notebook here ( https://colab.research.google.com/drive/1BSu3M-BA8G7_uLGOvIfIU77w0QPOk1Vn ) which checks that the installation works and demonstrates in a few lines what the subject is about. It runs in the browser with no installation at all, and the cells can equally be copied into a notebook on your own machine.