Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)
In 1963, meteorologist Edward Lorenz simulated a drastically simplified model of atmospheric convection on an early computer and found something startling: the trajectory never settled into a fixed point or a repeating cycle, tracing out instead an infinite, never-closing double-spiral shape resembling a butterfly's wings, and tiny changes in the starting point led to wildly different long-term paths. This is the origin of the popular idea of the "butterfly effect".
But a computer simulation, however striking the picture, is not a proof: floating-point round-off errors accumulate in a chaotic system, so the picture on the screen might just be numerical noise dressed up to look like genuine chaos, rather than a real mathematical object. In 1998, Steve Smale listed this as problem on his list of mathematical challenges for the 21st century: prove, rigorously, that Lorenz's picture is real.
The Lorenz equations , , arose as a brutal truncation of a Fourier expansion of Rayleigh–Bénard convection — Lorenz kept only three modes — and at they display the famous two-lobed attractor in every numerical simulation. But simulation is not proof: floating-point trajectories shadow nothing rigorous, and the observed behaviour is logically compatible with an astronomically long stable periodic orbit, or with an attractor that exists only inside the accumulation of rounding error.
Smale listed the question as problem 14 of his 1998 "Mathematical Problems for the Next Century": does the Lorenz system at the classical parameters support a strange attractor that is robust — persisting under small perturbations of the vector field? The obstruction to a classical proof is structural. The origin is a saddle equilibrium lying inside the attractor itself, so the system is singular-hyperbolic rather than uniformly hyperbolic: trajectories pass arbitrarily close to the saddle, where contraction in two directions meets expansion in one, and the return time to any cross-section grows without bound near the stable manifold.
Tucker's 1999 proof (the full details appear in "A rigorous ODE solver and Smale's 14th problem", Found. Comput. Math. 2002) answers the problem affirmatively by splitting phase space into a neighbourhood of the origin, treated by exact analysis, and its complement, treated by interval-arithmetic computation verified to machine-tight error bounds — the first example of a genuinely open dynamical-systems question settled by validated numerics.
- Strange attractor
- A bounded region in phase space that nearby trajectories are drawn into and never leave, but on which motion is chaotic (sensitive to initial conditions) rather than periodic; its cross-section typically has a fractal, non-integer-dimensional structure.
- Saddle equilibrium
- A fixed point of a dynamical system where trajectories are attracted along some directions but repelled along others, like a ball balanced on a horse saddle: stable if nudged forward-backward, unstable if nudged left-right.