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)

Số học khoảng thay mỗi số thực $x$ trong một tính toán bằng một khoảng compact $[\underline{x},\overline{x}]$ đảm bảo chứa nó, và định nghĩa lại các phép toán số học sao cho, ví dụ, $[\underline a,\overline a] + [\underline b,\overline b] = [\underline a+\underline b, \overline a + \overline b]$ và tương tự (với việc chia trường hợp phù hợp theo dấu) cho phép nhân và các phép toán khác; áp dụng một phiên bản mở rộng khoảng của một hàm cho một đối số khoảng đảm bảo tạo ra một khoảng chứa miền giá trị thực của hàm trên đối số đó. Ghép các phép toán như vậy lại, toàn bộ một thuật toán số học (ở đây, một bộ tích phân chuỗi Taylor bậc cao để giải các phương trình vi phân Lorenz) có thể chạy trên các đầu vào giá trị khoảng để tạo ra các đầu ra giá trị khoảng, được chứng thực toán học, với cái giá là các khoảng rộng ra hơn phần nào so với sai số dấu phẩy động thực ở mỗi bước ("hiệu ứng bao bọc" nổi tiếng, được kiểm soát trong thực tế bằng các kỹ thuật như phương pháp Lohner).

Kỹ thuật này, phát triển từ những năm 1960 trở đi (Ramon Moore) và được tinh chỉnh cho tích phân phương trình vi phân chặt chẽ bởi các tác giả bao gồm Lohner và Neumaier, chính xác là điều cho phép một chương trình máy tính hữu hạn, dấu phẩy động tạo ra một kết luận chặt chẽ về mặt toán học: thay vì theo dõi xấp xỉ một quỹ đạo duy nhất, cài đặt của Tucker theo dõi toàn bộ các hộp nhỏ (tích của các khoảng) điều kiện ban đầu và ảnh đảm bảo của chúng dưới dòng chảy, nên bất kỳ khẳng định nào được chứng minh về nơi một hộp điểm có thể kết thúc đều là một định lý được chứng thực, không phải một quan sát số học.

Với công cụ này sẵn có, phần còn lại của chứng minh Tucker (bên ngoài khối lập phương nhỏ $U_0$ được xử lý giải tích ở các bước trước) tiến hành bằng tính toán khoảng chặt chẽ thay vì mô phỏng suy nghiệm.