解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)
ローレンツのシミュレーションから36年後、そしてスメイル自身のリストが示唆する期限の1年前、Tuckerの証明はこの問いに決定的な決着をつけた:ローレンツの画面上の絵は幻影ではなかった。古典的ローレンツ方程式は、何十年もの数値実験が示唆してきた通り、真に頑健でカオス的なアトラクタを持つ。しかし今やそれは、どれほどの丸め誤差も揺るがすことのできない証明書に裏付けられている。
この成果はまた、その手法自体にとっても画期的なものである:これは力学系における最初の主要な結果の一つであり、コンピュータ支援による区間演算検証が、単なる有用な例示ではなく、証明の不可欠で代替不可能な要素であった。これは、カオス的力学系における計算機支援証明という、その後の研究プログラム全体への扉を開いたのである。
前段階で検証された三つの要素をGuckenheimer–Williamsの定理と組み合わせると、Tuckerの主結果が得られる: における古典的Lorenz系は頑健なストレンジアトラクタを持つ。ここで「頑健」とは、有限で厳密な計算がパラメータおよび数値の両方について小さいが明示的な誤差の余地を持つため、あらゆる近傍のパラメータ値についても同じ定性的結論が成り立つことを意味する;それはまた、アトラクタがいかなる特定の有限精度シミュレーションの数値的産物でもなく、カオスを装う非常に長周期の安定軌道でもないことを意味する。これによりSmaleの1998年のリスト「次の世紀のための数学的問題」の問題 が解決される。
この結果は、まずTuckerの1999年のノート「The Lorenz attractor exists」(Comptes Rendus de l'Académie des Sciences, Série I, 第328巻, pp. 1197–1202)で発表され、完全な論証と技術的詳細は「A rigorous ODE solver and Smale's 14th problem」(Foundations of Computational Mathematics, 2002年)で公表された。この論文はまた、計算を実行するために開発された、汎用の検証済み常微分方程式積分ソフトウェアについても記述している。
この特定の問題を閉じることを超えて、Tuckerの証明は、完全に説明された誤差評価を伴う区間演算に基づいて構築された計算機支援証明が、連続力学系における真に未解決の問いを解決しうることを最初に示した実例の一つとして歴史的に重要である—この方法論はその後、Tuckerや他の研究者によって、厳密数値計算やカオス的力学系におけるさらなる問題へと拡張されている。