Xếp cam

Bạn có một đống cam sành, vỏ rất rắn. Làm sao xếp chúng vào một cái hộp có thể tích bé nhất ?  Hay nói cách khác, phần trống giữa các quả cam có thể tích ít nhất.  Để làm toán cho dễ, ta tưởng tượng tất cả các quả cam to tròn bằng nhau, và đều rất chua.

Bài toán này được Kepler đặt ra vào năm 1611. Ông vẽ ra hai cách xếp cam, cả hai đều xếp đầy đươc chừng 3/4 thể tích của hộp (số chính xác là ).  Các bác bán cam thật ra đã dùng các cách xếp này để bày cam ngoài chợ trước Kepler từ lâu. Nhưng Kepler hơn các bác ở chỗ ông nghĩ rằng không thể xếp nhiều hơn nữa, mặc dầu ông không chứng minh được.  Cái này về sau trở thành một bài toán rất nổi tiếng là giả thuyết Kepler trong hình học tổ hợp.

Cách đây hơn chục năm, có bác Hales viết một chứng minh vô cùng dài về giả thuyết Kepler. Cách của bác dùng máy tính rất nhiều (250 trang + 3gigabit dữ liệu) và rất phức tạp.  Mặc dầu báo Annals of Math.  uy tín đã đăng, nhưng các phản biện cũng nói thẳng ra là họ không chắc 100% về các tính toán trong bài. Bác H. được tặng giải Fulkerson năm 2009.

Không chắc là không chắc thế nào ? Bác H. cáu, và quyết phải làm cho ra nhẽ. Trong vòng 10 năm, bác viết một chương trình  gọi là Flyspeck, với mục đích dùng máy tính kiểm tra tính chính xác của cách chứng minh. Dự án này một phần được thực hiện ở Việtnam (xem báo Thông tin toán học, 2015). Theo công bố gần đây của bác H. và đồng nghiệp, chương trình của bác đã thành công rực rỡ và xác định rằng chứng minh trước đó của bác là đúng 100%.

Mình thì chắc chắn là chứng minh của bác đúng rồi, cóc cần anh Flyspeck, vì bác là người yêu Việtnam, đến làm việc rất thường xuyên. Nhưng cái anh Flyspeck này, lại gợi ra lắm vấn đề.

Thứ nhất, thật thà mà nói  người ta muốn chứng minh một giả thuyết toán học là vì muốn biết tại sao nó đúng, đằng sau nó thực sự là vấn đề gì, những ý tưởng trong chứng minh dùng được vào việc gì khác vv, chứ còn bản thân cái sự đúng của giả thuyết không mấy quan trọng.  Bản thân cái mệnh đề của bài toán Fermat đúng hay sai không có ảnh hưởng gì lớn, vì ít ai dùng nó làm gì, cái ảnh hưởng lớn là các ý tưởng (nhiều khi được phát triển lên thành cả một lý thuyết) để giải quyết bài toán này. Việc này Flyspeck không làm được, và các ý tưởng lớn sau chứng minh của giả thuyết Kepler là gì, có vẻ ít người biết.

Vấn đề thứ hai liên quan môt chút về mặt kỹ thuật. Chương trình Flyspeck chạy mất mấy nghìn giờ, hiển nhiên các tính toán thao tác của nó rất phức tạp. Cu máy tính cũng thỉng thoảng sổ mũi hắt hơi. Nhỡ trong mấy nghìn giờ đấy nó sai lỗi đánh máy, bố ai biết được.  Sai số trong các tính toán máy tính, lúc nào cũng có. Chỉ có điều trong các bài toán định lượng, nó không đánh kể lắm. Chẳng hạn kết quả chính xác là 342.029988356  mà máy tính tính ra là 342.029988357, thì trong ứng dụng không có thay đổi gì lớn. (Vả lại ta cũng không biết kết quả chính xác là gì để so sánh.)   Nhưng khi câu trả lời là định tính, 0 hoặc 1, thì có thể tình hình sẽ khác. Bạn có thể tưởng tượng máy tính phải cộng 10 tỷ tỷ tỷ số nguyên, mỗi số là 1 hoặc 0, nếu chẳng hạn một số bị flip từ 0 sang 1 hay ngược lại, kết quả cuối cùng không thay đổi bao nhiêu. Nhưng nếu ta chỉ quan tâm đến kết quả cuối cùng là chẵn hay lẻ thôi, vấn đề thay đổi hoàn toàn.