Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)

The Lorenz system $\dot{x} = \sigma(y - x)$, $\dot{y} = x(\rho - z) - y$, $\dot{z} = xy - \beta z$ is a drastic (and physically unrealistic, but mathematically rich) truncation of the equations for Rayleigh–Bénard convection, published by Edward Lorenz in 1963. For the classical parameter values $(\sigma,\rho,\beta)=(10,28,8/3)$, numerical simulation strongly suggests trajectories settle onto a bounded, intricately folded, two-lobed "strange attractor" with sensitive dependence on initial conditions — the mathematical signature of chaos.

However, as recorded in Smale's 1998 list "Mathematical Problems for the Next Century" (problem $14$), no rigorous proof existed that this numerically observed object was a genuine mathematical attractor, as opposed to, say, an extremely long-period stable periodic orbit that only looks chaotic within the limits of floating-point precision, or an artifact of accumulated rounding error. The difficulty is structural: the origin $(0,0,0)$ is a saddle-type equilibrium of the system, and trajectories on the attractor pass arbitrarily close to it infinitely often; near a saddle, the time to return to a fixed cross-section blows up without bound, so naive fixed-precision numerical integration cannot certify what happens as a trajectory threads this bottleneck — a tiny numerical error there can be amplified into a completely different itinerary thereafter.

Warwick Tucker's 1999 proof, described in the coming steps, resolves problem $14$ by combining exact analytic estimates exactly where numerical methods fail (near the origin) with a rigorous, error-controlled computer verification everywhere else.