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

在小立方体 $U_0$ 之外,Tuckerは平面 $\{z=27\}$ 内の二次元Poincaré断面 $\Sigma$ を固定する(原点の鞍点の上に位置し、アトラクタと横断的に交わるために選ばれる)。そして $\Sigma$ の関連部分を、数千個の小さな長方形 $\{R_i\}$ からなる細かいメッシュに分割する。各長方形 $R_i$ について、Lorenz流の区間演算に基づく厳密な数値積分により、$\Sigma$ への初回帰還写像 $P$ のもとでの $R_i$ の真の像を含むことが保証された箱 $\widehat{P}(R_i) \supset P(R_i)$ を計算する(軌道がたまたま $U_0$ を通過するときは前段階の解析的評価を差し込む)。

各長方形について、$\widehat{P}(R_i)$ が合併 $\bigcup_i R_i$ に含まれることを確認することで、この合併が前方不変であることが証明される:その中で始まる軌道はそこから決して出られない。これは、Lorenzの絵に対して論理的に可能な二つの失敗モードのうちの一つ—見かけ上のアトラクタが実際には有界でないこと、あるいは浮動小数点誤差を厳密に考慮するとまったく異なる長期的挙動へ漏れ出ることを排除する。

それ自体では、前方不変性はある有界で複雑な集合が流れを罠にかけることを示すにすぎない;その罠にかけられた領域内での運動がカオス的であるか、それともひそかに長周期の安定軌道であるかについては何も語っていない。その区別は次の段階の主題である。