Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)
Thirty-six years after Lorenz's simulation and one year before the deadline implied by Smale's own list, Tucker's proof settled the question definitively: the picture on Lorenz's screen was not a mirage. The classical Lorenz equations genuinely possess a robust, chaotic attractor, exactly as decades of numerical experiments had suggested, but now backed by a certificate no amount of round-off error could undermine.
The achievement is also a landmark for the method itself: it is one of the first major results in dynamical systems where computer-assisted, interval-arithmetic verification was not just a helpful illustration but an essential, irreplaceable ingredient of the proof — opening the door to an entire subsequent research programme of computer-assisted proofs in chaotic dynamics.
Combining the three verified ingredients from the previous step with the Guckenheimer–Williams theorem yields Tucker's main result: the classical Lorenz system at has a robust strange attractor. "Robust" here means the same qualitative conclusion holds for every nearby parameter value, since the finite, rigorous computation carries a small but explicit margin of error in the parameters as well as in the numerics; it also means the attractor is not a numerical artifact of any particular finite-precision simulation, nor a very-long-period stable orbit masquerading as chaos. This resolves problem on Smale's 1998 list of "Mathematical Problems for the Next Century".
The result was first announced in Tucker's 1999 note "The Lorenz attractor exists" (Comptes Rendus de l'Académie des Sciences, Série I, vol. 328, pp. 1197–1202), with the complete argument and full technical details published in "A rigorous ODE solver and Smale's 14th problem" (Foundations of Computational Mathematics, 2002), which also describes the general-purpose validated ODE-integration software developed to carry out the computation.
Beyond closing this specific problem, Tucker's proof is historically significant as one of the first demonstrations that computer-assisted proof, when built on interval arithmetic with fully accounted-for error bounds, can settle genuinely open questions in continuous dynamical systems — a methodology since extended by Tucker and others to further problems in rigorous numerics and chaotic dynamics.