A rigorous ODE solver and Smale's 14th problem (Q1601363)

The author presents an algorithm for computing rigorous solutions for ordinary differential equations. The algorithm is broken down into two main parts: A local part, which is based on normal form theory, and a global part, which involves interval arithmetic with directed rounding and partitioning process. As an application of this algorithm, the author proves that the Lorenz equations support a robust strange attractor and that its flow admits a unique SRB measure, whose support coincides with the attractor.