A Verified ODE Solver and the Lorenz Attractor

Abstract

A rigorous numerical algorithm, formally verified with Isabelle/HOL, is used to certify the computations that Tucker used to prove chaos for the Lorenz attractor. The verification is based on a formalization of a diverse variety of mathematics and algorithms. Formalized mathematics include ordinary differential equations and Poincaré maps. Algorithms include low level approximation schemes based on Runge–Kutta methods and affine arithmetic. On a high level, reachability analysis is guided by static hybridization and adaptive step-size control and splitting. The algorithms are systematically refined towards an implementation that can be executed on Tucker’s original input data.