Validated numerical proofs

Lecturer

Dr. Liam Hodgkinson, The University of Melbourne

Synopsis

The most profound problems in mathematics remain “hard” because they resist simple analytical closure. Fortunately, history has shown that computational assistance can break the barrier to a solution. Landmark results, including the Kepler Conjecture and verification of the Lorenz Attractor, were only made possible by leveraging the computer to resolve the dense, intractable inequalities that traditional methods could not tame. This course explores the frontier of validated numerics, where we leverage the speed of modern computers not just to provide evidence of a claim, but to prove it. By replacing traditional heuristic estimates with refined, computer-assisted enclosures, we can overcome the limitations of standard analysis, treating the computer as a formal extension of the logical proof process.

• 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

• TBA

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.