A Verified ODE Solver and Smale's 14th Problem

Duration: 48 mins 38 secs

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/2523787/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Immler, F Thursday 6th July 2017 - 13:40 to 14:20


Created:	2017-07-24 11:34
Collection:	Big proof
Publisher:	Isaac Newton Institute
Copyright:	Immler, F
Language:	eng (English)


Abstract:	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.

Abstract:

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.

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.91 Mbits/sec	697.66 MB	View	Download
WebM	640x360	438.74 kbits/sec	156.34 MB	View	Download
iPod Video	480x270	492.7 kbits/sec	175.50 MB	View	Download
MP3	44100 Hz	249.76 kbits/sec	89.06 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)