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

Interval arithmetic replaces each real number $x$ in a computation with a compact interval $[\underline{x},\overline{x}]$ guaranteed to contain it, and redefines the arithmetic operations so that, for example, $[\underline a,\overline a] + [\underline b,\overline b] = [\underline a+\underline b, \overline a + \overline b]$ and similarly (with appropriate case-splitting on signs) for multiplication and other operations; applying an interval-extended version of a function to an interval argument is guaranteed to produce an interval containing the function's true range over that argument. Composing such operations, an entire numerical algorithm (here, a high-order Taylor-series integrator for solving the Lorenz ODEs) can be run on interval-valued inputs to produce interval-valued, mathematically certified outputs, at the cost of the intervals growing somewhat wider than the true floating-point error at each step (the well-known "wrapping effect", controlled in practice using techniques such as Lohner's method).

This technique, developed from the 1960s onward (Ramon Moore) and refined for rigorous ODE integration by authors including Lohner and Neumaier, is precisely what lets a finite, floating-point computer program produce a mathematically airtight conclusion: rather than tracking a single trajectory approximately, Tucker's implementation tracks entire small boxes (products of intervals) of initial conditions and their guaranteed images under the flow, so that any statement proved about where a box of points can end up is a certified theorem, not a numerical observation.

With this tool available, the rest of Tucker's proof (outside the small cube $U_0$ handled analytically in the previous steps) proceeds by rigorous interval computation rather than heuristic simulation.