解法：塔克利用区间算术给出的严格计算机辅助证明(1999年)
通俗地说
在原点附近的小立方体之外,塔克选取一个切过吸引子的平面截面(平面 ),把它切成数千个微小的矩形。对每一个矩形,他要求计算机用区间算术计算出一个有保证的包络,精确界定该矩形中每一点在其轨道下一次穿过截面时会落到何处。
通过检验每一个矩形对应的包络都落回所有矩形并集之内,塔克证实了一个具体的、被精确界定的区域是一个陷阱:轨道一旦进入其中,无论追踪多久都永远无法逃离。仅这一事实就排除了吸引子偷偷漏向无穷远,或漏向空间中完全不同部分的可能性。
详细分析
在小立方体 之外,塔克在平面 内固定一个二维庞加莱截面 (之所以选它,是因为它位于原点鞍点上方,并且与吸引子横截相交),并把 的相关部分划分成由数千个小矩形 组成的精细网格。对每个矩形 ,一次基于区间算术的严格数值积分(计算洛伦兹流)会给出一个盒子 ,保证包含 在首次回归映射 到 下的真实像(每当轨道恰好经过 时,就拼接进前面步骤中的解析估计)。
逐个矩形地检验 都包含在并集 之内,就证实了这个并集是前向不变的:从中出发的轨道永远无法离开它。这排除了洛伦兹图像在逻辑上两种可能的失败模式之一——即所谓的吸引子实际上并不有界,或者一旦严格考虑浮点误差就会漏向某种完全不同的长期行为。
单凭前向不变性,只能说明某个有界的、复杂的集合困住了流;它还没有说明这个被困区域内部的运动究竟是混沌的,还是暗中是一个长周期的稳定轨道。这一区分正是下一步的主题。