skip to content

A Verified ODE Solver and Smale's 14th Problem

Presented by: 
Fabian Immler
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.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons