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

区间算术把计算中的每个实数 $x$ 替换为一个保证包含它的紧致区间 $[\underline{x},\overline{x}]$,并重新定义算术运算,使得例如 $[\underline a,\overline a] + [\underline b,\overline b] = [\underline a+\underline b, \overline a + \overline b]$,乘法及其他运算也类似(需按符号做适当分类讨论);把一个函数的区间扩展版本应用于某个区间自变量,可以保证得到一个包含该函数在此自变量上真实值域的区间。把这类运算组合起来,一整套数值算法(这里是用于求解洛伦兹常微分方程组的高阶泰勒级数积分器)就可以在区间值输入上运行,产生区间值的、经过数学认证的输出,代价是每一步区间会比真实的浮点误差稍微变宽一些(著名的「包裹效应」,在实践中可用 Lohner 方法等技术加以控制)。

这一技术从1960年代起(Ramon Moore)发展,并由 Lohner、Neumaier 等人为严格的常微分方程积分加以完善,正是它使得一个有限的、基于浮点数的计算机程序能够得出数学上滴水不漏的结论:塔克的实现所追踪的不是对单条轨道的近似,而是初始条件的整块整块的小盒子(区间的乘积)以及它们在流下经保证的像,因此任何关于一盒点最终会落到哪里的、被证明的论断,都是一条经过认证的定理,而不是一次数值观测。

有了这个工具,塔克证明的其余部分(在前面步骤中已用解析方法处理的小立方体 $U_0$ 之外)就通过严格的区间计算而非启发式模拟来进行。