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.

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