Lời giải: Chứng minh chặt chẽ có máy tính hỗ trợ của Tucker bằng số học khoảng (1999)

Hệ phương trình Lorenz $\dot{x} = \sigma(y - x)$, $\dot{y} = x(\rho - z) - y$, $\dot{z} = xy - \beta z$ ra đời như một phép cắt cụt tàn nhẫn của khai triển Fourier cho đối lưu Rayleigh–Bénard — Lorenz chỉ giữ ba mode — và tại $(\sigma, \rho, \beta) = (10, 28, 8/3)$ chúng hiển thị attractor hai thùy nổi tiếng trong mọi mô phỏng số. Nhưng mô phỏng không phải chứng minh: quỹ đạo dấu phẩy động không bóng theo điều gì chặt chẽ, và hành vi quan sát được về logic vẫn tương thích với một quỹ đạo tuần hoàn bền cực dài, hoặc một attractor chỉ tồn tại trong sự tích luỹ sai số làm tròn.

Smale đưa câu hỏi thành bài 14 trong danh sách 1998 "Mathematical Problems for the Next Century": hệ Lorenz ở tham số cổ điển có nâng một strange attractor bền — tồn tại dưới nhiễu loạn nhỏ của trường vectơ — không? Rào cản cho một chứng minh cổ điển là cấu trúc. Gốc toạ độ là điểm yên ngựa nằm ngay trong attractor, nên hệ là singular-hyperbolic chứ không uniformly hyperbolic: quỹ đạo đi gần yên ngựa tuỳ ý, nơi co theo hai phương gặp giãn theo một phương, và thời gian quay lại mọi thiết diện phình vô hạn gần đa tạp bền.

Chứng minh 1999 của Tucker (chi tiết đầy đủ trong "A rigorous ODE solver and Smale's 14th problem", Found. Comput. Math. 2002) trả lời khẳng định bằng cách tách không gian pha thành một lân cận của gốc, xử lý bằng phân tích chính xác, và phần bù của nó, xử lý bằng tính toán số học khoảng được kiểm với chặn sai số chặt tới mức máy — ví dụ đầu tiên một câu hỏi hệ động lực thực sự mở được giải quyết bằng số học có thẩm định.