解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)
1963年、気象学者エドワード・ローレンツは大気対流の劇的に単純化されたモデルを初期のコンピュータでシミュレートし、驚くべきことを発見した:軌道は決して不動点や周期軌道に落ち着かず、代わりに蝶の羽根に似た、無限に閉じない二重螺旋の形を描き、出発点のわずかな違いがまったく異なる長期的な経路につながった。これが「バタフライ効果」という広く知られた発想の起源である。
しかし、コンピュータシミュレーションは、どれほど印象的な絵であっても証明ではない:カオス的な系では浮動小数点の丸め誤差が蓄積するため、画面上の絵は本物のカオスに見せかけただけの数値的なノイズにすぎないかもしれず、実在する数学的対象とは限らない。1998年、スティーブ・スメイルはこれを21世紀のための数学的課題リストの第 問として挙げた:ローレンツの絵が本物であることを厳密に証明せよ、と。
Lorenz 方程式 , , は Rayleigh–Bénard 対流の Fourier 展開の大胆な打ち切り——Lorenz が3つのモードだけを残したもの——として生まれ、 ではあらゆる数値シミュレーションで有名な二葉のアトラクタを示す。しかしシミュレーションは証明ではない：浮動小数点の軌道は厳密なものを何もシャドーせず、観察される振る舞いは天文的に長い安定周期軌道、あるいは丸め誤差の蓄積の中にのみ存在するアトラクタと論理的に両立する。
Smale はこの問題を1998年の「Mathematical Problems for the Next Century」の問題14として挙げた：古典的パラメータでの Lorenz 系はロバストな——ベクトル場の小さな摂動の下で存続する——ストレンジアトラクタを持つか？古典的証明への障害は構造的である。原点はアトラクタ自身の内部にある鞍点平衡なので、系は一様双曲的ではなく特異双曲的である：軌道は鞍点に任意に近づき、そこでは2方向の収縮と1方向の拡大が出会い、安定多様体の近くでは任意の断面への戻り時間が際限なく大きくなる。
Tucker の1999年の証明（完全な詳細は「A rigorous ODE solver and Smale's 14th problem」, Found. Comput. Math. 2002）は、相空間を原点の近傍（厳密解析で扱う）とその補集合（機械精度までの誤差評価付き区間演算で扱う）に分割することで肯定的に答えた——検証済み数値計算で真に未解決だった力学系の問題が解決された最初の例である。
- ストレンジアトラクタ
- 近くの軌道が引き込まれ決して離れない、相空間内の有界な領域であるが、そこでの運動は周期的ではなく(初期条件に敏感な)カオス的である。その断面は通常、フラクタルで非整数次元の構造を持つ。
- 鞍点型平衡点
- 力学系の不動点で、一部の方向に沿っては軌道が引き寄せられるが、他の方向に沿っては反発される点。馬の鞍の上に置かれたボールのようなもので、前後に押すと安定だが、左右に押すと不安定である。