解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)

区間演算は、計算中のあらゆる実数 $x$ を、それを含むことが保証されたコンパクトな区間 $[\underline{x},\overline{x}]$ に置き換え、算術演算を再定義する。例えば $[\underline a,\overline a] + [\underline b,\overline b] = [\underline a+\underline b, \overline a + \overline b]$ であり、乗算やその他の演算についても(符号に応じた適切な場合分けにより)同様である;関数の区間拡張版を区間の引数に適用すると、その引数にわたる関数の真の値域を含む区間を生成することが保証される。このような演算を合成することで、数値アルゴリズム全体(ここではLorenz常微分方程式を解くための高次Taylor級数積分器)を区間値の入力に対して実行し、区間値の、数学的に証明された出力を生成できる。代償として、各ステップで区間が真の浮動小数点誤差よりもいくらか広がる(いわゆる「ラッピング効果」であり、Lohnerの方法などの手法によって実際には制御される)。

1960年代以降(Ramon Moore)発展し、Lohner や Neumaier を含む著者らによって厳密な常微分方程式積分のために洗練されたこの技法こそが、有限の浮動小数点コンピュータプログラムに数学的に鉄壁な結論を出させることを可能にする:単一の軌道を近似的に追跡する代わりに、Tuckerの実装は初期条件の小さな箱(区間の積)全体と、流れの下でのその保証された像を追跡する。したがって、点の箱がどこに行き着きうるかについて証明されたどんな主張も、数値的な観察ではなく証明された定理となる。

この道具が利用可能になったことで、Tuckerの証明の残りの部分(前段階で解析的に扱われた小さな立方体 $U_0$ の外側)は、発見的なシミュレーションではなく厳密な区間計算によって進められる。