解法：塔克利用区间算术给出的严格计算机辅助证明(1999年)

Lorenz 方程 $\dot{x} = \sigma(y - x)$, $\dot{y} = x(\rho - z) - y$, $\dot{z} = xy - \beta z$ 源自对 Rayleigh–Bénard 对流 Fourier 展开的粗暴截断——Lorenz 只保留三个模——在 $(\sigma, \rho, \beta) = (10, 28, 8/3)$ 处一切数值模拟都显示著名的双叶吸引子。但模拟不是证明：浮点轨道并不严格地“影子”任何真实轨道，且所观测的行为在逻辑上仍可能与一条天文长度级的稳定周期轨道相容，或与只存在于舍入误差累积之内的吸引子相容。

Smale 把此问题列为他 1998 年“下世纪数学问题”的第 14 题：经典参数下的 Lorenz 系统是否具有一个鲁棒的奇怪吸引子——即在向量场的小扰动下依然存续？古典证明的障碍是结构性的。原点是位于吸引子内部的鞍型平衡点，因此系统是奇异双曲而非一致双曲：轨道可以任意接近鞍点，在那里两方向的收缩与一方向的扩张相遇，且向任何截面的回归时间在稳定流形附近无界增长。

Tucker 1999 年的证明（完整细节见 “A rigorous ODE solver and Smale's 14th problem”, Found. Comput. Math. 2002）给出了肯定答案：他把相空间分为原点邻域（用精确分析处理）与其补集（用误差界精确到机器精度的区间算术计算处理）——这是经验证数值方法首次解决一个真正未决的动力系统问题。