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

Lorenz系 $\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)$ は系の鞍点型平衡点であり、アトラクタ上の軌道は無限回それに任意に近づく;鞍点の近くでは、固定された断面への帰還時間が無限に発散するため、素朴な固定精度の数値積分では、軌道がこのボトルネックを通り抜けるときに何が起こるかを保証できない—そこでのわずかな数値誤差が、その後まったく異なる軌跡へと増幅されうる。

次の段階で説明されるWarwick Tuckerの1999年の証明は、数値的手法が失敗するまさにその場所(原点付近)での厳密な解析的評価と、それ以外のすべての場所での誤差が制御された厳密なコンピュータ検証とを組み合わせることで、問題 $14$ を解決する。