解法：塔克利用区间算术给出的严格计算机辅助证明(1999年)
在洛伦兹的模拟出现三十六年后、也是斯梅尔自己清单所暗示的期限之前一年,塔克的证明彻底解决了这个问题:洛伦兹屏幕上的图像并非幻觉。经典的洛伦兹方程确实拥有一个稳健的混沌吸引子,正如数十年来的数值实验所暗示的那样,而如今它得到了一份任何舍入误差都无法撼动的证书的支持。
这一成就本身对这种方法而言也是一座里程碑:它是动力系统领域中最早的重大成果之一,其中计算机辅助的区间算术验证不仅仅是有益的例示,而是证明中不可或缺、无可替代的组成部分——由此开启了此后整整一个关于混沌动力学中计算机辅助证明的研究计划。
把前一步中验证过的三个要素与古根海默–威廉姆斯定理结合起来,就得到塔克的主要结果:在 处,经典的洛伦兹系统拥有一个稳健的奇异吸引子。这里的「稳健」是指同样的定性结论对每一个邻近的参数值也成立,因为那个有限的、严格的计算无论在参数上还是在数值上,都带有一个小而明确的误差余量;它也意味着这个吸引子既不是任何特定有限精度模拟的数值伪影,也不是伪装成混沌的、周期极长的稳定轨道。这解决了斯梅尔1998年清单《下个世纪的数学问题》中的第 题。
这一结果首先在塔克1999年的短文《洛伦兹吸引子存在》(Comptes Rendus de l'Académie des Sciences,第一辑,第328卷,第1197–1202页)中公布,完整论证与全部技术细节则发表于《一个严格的常微分方程求解器与斯梅尔第14题》(Foundations of Computational Mathematics,2002年),该文还描述了为完成这一计算而开发的通用验证型常微分方程积分软件。
除了终结这个具体问题之外,塔克的证明在历史上也具有里程碑意义,它是最早证明计算机辅助证明——当建立在带有完整误差界的区间算术之上时——能够解决连续动力系统中真正开放问题的实例之一,此后这一方法论已被塔克与其他学者推广到严格数值计算与混沌动力学中的更多问题上。