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ệ Lorenz $\dot{x} = \sigma(y - x)$, $\dot{y} = x(\rho - z) - y$, $\dot{z} = xy - \beta z$ là một sự cắt cụt mạnh (và không thực tế về mặt vật lý, nhưng phong phú về mặt toán học) của các phương trình đối lưu Rayleigh–Bénard, được Edward Lorenz công bố năm 1963. Với các giá trị tham số cổ điển $(\sigma,\rho,\beta)=(10,28,8/3)$, mô phỏng số học gợi ý mạnh mẽ rằng quỹ đạo ổn định vào một "hút tử lạ" bị chặn, gấp nếp phức tạp, hai thùy, có tính nhạy cảm với điều kiện ban đầu — dấu hiệu toán học của hỗn loạn.

Tuy nhiên, như được ghi trong danh sách năm 1998 của Smale "Mathematical Problems for the Next Century" (bài toán $14$), không có chứng minh chặt chẽ nào tồn tại rằng đối tượng quan sát được bằng số học này là một hút tử toán học thực sự, thay vì, chẳng hạn, một quỹ đạo ổn định chu kỳ cực dài chỉ trông có vẻ hỗn loạn trong giới hạn độ chính xác dấu phẩy động, hay một sản phẩm phụ của sai số làm tròn tích lũy. Khó khăn mang tính cấu trúc: gốc tọa độ $(0,0,0)$ là một điểm cân bằng kiểu yên của hệ, và quỹ đạo trên hút tử đi qua tùy ý gần nó vô hạn lần; gần một điểm yên, thời gian hồi quy về một mặt cắt cố định tăng vọt không giới hạn, nên phép tích phân số học độ chính xác cố định ngây thơ không thể chứng thực điều gì xảy ra khi quỹ đạo xuyên qua nút thắt cổ chai này — một sai số số học nhỏ ở đó có thể được khuếch đại thành một hành trình hoàn toàn khác sau đó.

Chứng minh năm 1999 của Warwick Tucker, được mô tả ở các bước tiếp theo, giải quyết bài toán $14$ bằng cách kết hợp các ước lượng giải tích chính xác đúng ở nơi phương pháp số học thất bại (gần gốc tọa độ) với một sự xác thực bằng máy tính chặt chẽ, kiểm soát được sai số ở mọi nơi khác.