skip to content

A Verified ODE Solver and Smale's 14th Problem

Presented by: 
Fabian Immler Technische Universität München
Thursday 6th July 2017 - 13:40 to 14:20
INI Seminar Room 2
Smale's 14th Problem is a conjecture about chaos in a
particular dynamical system, the Lorenz attractor. The problem was solved by
Warwick Tucker with a combination of regular analysis and a computer-assisted
part. The computer-assisted part yields numerical bounds on solutions of the
Lorenz ODE, which are required to certify chaos.

In this talk, I will present the current library of ODEs
and verified numerical methods in Isabelle/HOL, and how I use it for a formal
verification of the computer-assisted part of Tucker's proof.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons