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

洛伦兹系统 $\dot{x} = \sigma(y - x)$、$\dot{y} = x(\rho - z) - y$、$\dot{z} = xy - \beta z$ 是对瑞利–贝纳德对流方程的一种大幅(在物理上不真实、但数学上极为丰富的)截断,由爱德华·洛伦兹于1963年发表。对于经典参数值 $(\sigma,\rho,\beta)=(10,28,8/3)$,数值模拟强烈暗示轨道会稳定到一个有界的、折叠得错综复杂的双叶「奇异吸引子」上,并对初始条件具有敏感依赖性——这正是混沌的数学标志。

然而,正如斯梅尔在1998年的清单《下个世纪的数学问题》(第 $14$ 题)中所记载的,当时并不存在严格的证明来说明这个数值观测到的对象是真正的数学吸引子,而不是,比如说,一个仅在浮点精度限度内看起来混沌的、周期极长的稳定周期轨道,或者只是累积舍入误差的产物。这一困难是结构性的:原点 $(0,0,0)$ 是该系统的一个鞍型平衡点,吸引子上的轨道会无穷次地任意接近它;在鞍点附近,回到某个固定截面的回归时间会无限发散,因此朴素的定精度数值积分无法证实轨道穿过这个瓶颈时究竟发生了什么——那里微小的数值误差此后可能被放大成完全不同的轨迹。

沃里克·塔克 1999 年的证明(在接下来的步骤中描述)正是通过在数值方法失效之处(原点附近)采用精确的解析估计,并在其余各处采用严格的、误差可控的计算机验证,来解决第 $14$ 题的。