Việc một bài toán đã tồn tại 400 năm nay được chứng minh bằng máy tính có thể mở ra một kỷ nguyên mới cho toán học, trong đó máy tính thực hiện các công việc kỹ năng để giải phóng con người cho những suy luận sâu sắc hơn.
Bài toán này là một câu hỏi quen thuộc với những người bán hoa quả ở khắp mọi nơi: Xếp những quả cam thế nào là tốt nhất? Năm 1611, nhà toán học và thiên văn học người Đức Johannes Kepler cho rằng cách sắp xếp theo hình kim tự tháp là hiệu quả nhất, nhưng không thể chứng minh được điều này.
 |
| Johannes Kepler (27/12/1571-15/11/1630) |
Suy diễn trực giác của Kepler (mà ngày nay được gọi là giả thuyết Kepler) có thể phát biểu về mặt toán học như sau: Cách thức xếp các khối cầu cùng kích thước trong không gian theo kiểu hình kim tự tháp có mật độ chiếm không gian trung bình lớn nhất trong tất cả các cách xếp. Mật độ trung bình của kiểu √ xếp này có thể tính chính xác là π/3 2. Giả thuyết này là một phần của vấn đề thứ 18 trong danh mục 23 vấn đề nổi tiếng do Hilbert nêu ra năm 1900. Có thể xem cuốn sách [4] để thấy tầm ảnh hưởng của giả thuyết Kepler trong lịch sử toán học.
Gần đây, Thomas Hales, giáo sư của Đại học Pittsburgh, Pennsylvania, thông báo đã hoàn thành một nỗ lực hùng tráng nhằm chứng minh một cách hình thức suy diễn trên của Kepler. Ông nói "Vai tôi đã trút được một gánh nặng khổng lồ" và "Tôi bỗng nhiên cảm thấy trẻ ra mười tuổi!" Tại sao Hales lại nói như vậy và thế nào là một chứng minh hình thức?
Năm 1998 Hales lần đầu đưa ra chứng minh suy diễn trực giác của Kepler là đúng. Mặc dù có vô hạn cách để xếp các khối cầu, nhưng phần lớn chúng chỉ là biến thể của vài ngàn cấu hình. Hales đã phân chia các khả năng sắp xếp vô hạn khối cầu thành khoảng 2500 cách sắp xếp 50 khối cầu về mặt toán học, rồi sau đó dùng máy tính để kiểm tra mật độ tất cả các cách sắp xếp này. Tuy nhiên đây là một chứng minh khủng khiếp dày 250 trang cùng với 3 gigabytes phần mềm tính toán mà 12 nhà phản biện đã phải mất tới 4 năm để kiểm tra. Cuối cùng tạp chí Annals of Mathematics cũng công bố bài báo của Hales năm 2005 kèm theo một thông báo là các phản biện không thể kiểm tra chứng minh của Hales có đúng hay không. Một tiền lệ chưa từng có! Nhà toán học Gabor Fejes Toth phát biểu rằng chỉ có thể khẳng định "chắc chắn 99 phần trăm" chứng minh là đúng do không thể kiểm chứng được phần tính toán của máy tính. Nhiều nhà toán học không thỏa mãn với chứng minh này của Hales.
Vì vậy, từ năm 2003, Hales bắt đầu chương trình Flyspeck (dựa theo các chữ đầu FPK của câu “Formal Proof of Kepler”), một nỗ lực nhằm xác minh chứng minh của mình là đúng thông qua một sự kiểm chứng hình thức. Điều này có nghĩa là máy tính sẽ kiểm tra các suy luận logic hình thức trong chứng minh có gì sai không. Nhóm nghiên cứu của Hales đã phát triển hai phần mềm trợ giúp chứng minh hình thức có tên gọi là Isabelle và HOL Light. Cả hai phần mềm này đều được xây dựng dựa trên một phần lõi logic đã được kiểm tra kỹ lưỡng là không có bất kỳ lỗi nào. Chúng đưa ra một nền tảng cho phép máy tính có thể kiểm tra bất cứ chuỗi mệnh đề logic nào nhằm xem chúng có đúng không. Có một điều thú vị là ngoài các kiểm chứng độc lập hai phần mềm trên, nhóm của Hales cũng dùng chính hai phần mềm này để tự kiểm tra xem chúng có lỗi không.
 |
| Thomas Callister Hales |
Phần đầu tiên của chương trình Flyspeck là phân loại tất cả đồ thị thuần hóa (tame graphs) trong phần mềm Is- abelle được thực hiện bởi Bauer và Nip- kow. Phần này liệt kê cấu trúc tổ hợp của các phản ví dụ tiềm năng cho giả thiết Kepler. Định lý phân loại của họ đã được dịch tương ứng sang phần mềm HOL Light. Phần thứ hai của dự án kiểm tra tính đúng đắn của tất cả các bất đẳng phi tuyến trong HOL dựa trên luận án của Solovyev năm 2012. Việc xác minh tính đúng đắn của tất cả các bất đẳng phi tuyến trong HOL sử dụng thuật toán đám mây Azure của Microsoft trong 5000 giờ. Hầu như tất cả các tính toán được thực hiện song song với 32 lõi, do đó thời gian thực sự là khoảng 5000/32 = 156,25 giờ. Phần cuối cùng của dự án là chứng minh giả thiết Kepler trong HOL Light. Việc xác minh tính đúng đắn của tất cả các chuỗi logic ở mức độ vi mô trong chứng minh giả thiết Kepler bằng phần mềm HOL Light được thực hiện bởi nhóm nghiên cứu Việt Nam trong 6 năm. Nhóm này gồm Triệu Thị Diệp, Đặng Tất Đạt, Vũ Khắc Kỷ, Vương Anh Quyền, Nguyễn Tất Thắng, Trần Nam Trung, Hoàng Lê Trường, Nguyễn Quang Trưởng,... [3]. Trong thời gian đó ông Hales đã nhiều lần đến Viện Toán học tổ chức các bài giảng và hội thảo về chương trình Flyspeck.
Vào ngày Chủ nhật 10 tháng 8, ngay trước thềm Đại hội Toán học Quốc tế (ICM) 2014, chương trình Flyspeck thông báo họ đã chuyển được chứng minh toán học của Hales sang dạng máy tính và kiểm chứng được rằng nó thực sự chính xác [3]. Tin này lập tức gây chấn động trong cộng đồng toán học. Nhiều tờ báo trên thế giới và Bản tin của ICM 2014 đã đồng loạt đưa tin về sự kiện này
"Công nghệ này loại bỏ các nhà phản biện khỏi quá trình kiểm tra chứng minh”, Hales nói. "Ý kiến của họ về tính chính xác của một chứng minh không còn là vấn đề". "Đó là một nỗ lực to lớn", Alan Bundy của Đại học Edinburgh, Anh, người không tham gia vào công việc này nói. Ông nói thêm rằng ông hy vọng sự thành công của chương trình Flyspeck sẽ khích lệ các nhà toán học khác bắt đầu sử dụng các phần mềm hỗ trợ chứng minh. "Một nhà toán học nổi tiếng thế giới đã sử dụng phép chứng minh định lý một cách tự động. Một sự kiện xã hội như vậy rất quan trọng", ông nói. "Đây là một trường hợp nghiên cứu có thể bắt đầu trở thành tiêu chuẩn."
Lý tưởng nhất, phần mềm hỗ trợ sẽ làm việc phía sau trong khi các nhà toán học có thể dồn tâm sức cho những ý tưởng mới. Phần mềm đã có thể tự chứng minh một số mệnh đề cơ bản, nhưng nó cần phải dễ dàng sử dụng hơn. "Chúng ta cần biết cách khai thác phép chứng minh để nhận được một bức tranh lớn", Bundy nói. "Việc xem xét mọi thứ ở tầng vi mô vượt quá khả năng của chúng ta. Là con người chúng ta không thể hấp thu quá nhiều."
Cũng cần nói thêm rằng phương pháp nghiên cứu của Hales đã giúp ông giải quyết được Bài toán tổ ong từ thế kỷ thứ ba trước Công nguyên. Bài toán này nói rằng việc chia một miền phẳng thành các phần có diện tích bằng nhau sẽ có tổng chu vi nhỏ nhất khi chia thành các lục giác đều theo kiểu tổ ong. Ngoài ra, phương pháp của Hales còn có thể có ứng dụng trong việc truyền tín hiệu trong công nghệ thông tin. Thông thường, người ta muốn cùng một lúc gửi đi càng nhiều tín hiệu càng tốt. Tuy nhiên truyền quá nhiều tín hiệu cùng một lúc sẽ gây ra nhiễu. Hales cho rằng “Vấn đề ở đây là mật độ tín hiệu như thế nào là tốt nhất”. Câu hỏi này cũng giống như bài toán xếp khối cầu trong toán học.
Đối với Hales, ông sẵn sàng để tiếp bước. "Tôi có một cái hộp tràn đầy những ý tưởng mà tôi phải đặt sang một bên khi làm việc với phép chứng minh hình thức này", ông nói. "Chúng ta hãy hy vọng rằng chương trình tiếp theo không mất tới 20 năm!"
Tài liệu tham khảo
- Jacob Aron, Proof confirmed of 400-year-old fruit-stacking problem. New Scientist 12.8.2014.
- Frank Morgan, Kepler’s Conjecture and Hales’s Proof. Notices of the AMS 52(1) (2005), 44-47.
- Flysspeck, Annoucement of completion, https://code.google.com/p/flyspeck/wiki/ An- nouncingCompletion
- George Szpiro, Kepler’s Conjecture: How some of the greatest minds in history helped solve one of the oldest math problems in the world. Wiley & Sons, 2003.
Hoàng Lê Trường