A Verified ODE Solver and Smale's 14th Problem

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.  The computer-assisted part of Tuckers proof has been formally verified
in the interactive theorem prover Isabelle/HOL. I will present Isabelle/HOL's library of ODEs and verified numerical methods and how they underpin the formal verification of the computer-assisted part.