Những bông tuyết và phép chứng minh

1. Vấn đề lâu đời nhất trong hình học rời rạc

Nhà thiên căn học vĩ đại Johannes Kepler đã viết một cuốn sách nhỏ năm 1611 tên là “Bông tuyết sáu góc”. Làm thế nào để giải thích tại sao bông tuyết lại có sáu góc? Ông đã viết lại rằng đó là vì bông tuyết được tạo bởi những khối tròn và sự sắp xếp của những khối này cho ta hình dạng của bông tuyết. Ý tưởng đơn giản này đã lóe sáng trong hai thế kỷ nghiên cứu về lĩnh vực tinh thể học.

Kepler đã mô tả vấn đề tương tự khi xếp kín các viên đạn và nói rằng đo là sự xếp kín tốt nhất theo nghĩa; Không có sự sắp xếp nào khác của các hình cầu đồng dạng mà có thể lấp đầy khoảng không gian lớn hơn cách sắp xếp này. Điều này được biết như là giả thuyết Kepler. Đó là một vấn đề lâu đời nhất trong thình học rời rạc và trải qua nhiều thế kỉ mà không có lời giải.

Tại sao một vấn đề dễ đặt ra như vậy mà khó giải đáp đến thế? Một nhà báo ở Plymouth, New Zealandđã đem câu hỏi này ra một khu chợ. Những người bán rau quả ở đó không hề ngạc nhiên với câu hỏi. “Bố tôi đã chỉ cho tôi làm thế nào để xếp các quả cam khi tôi mới bốn tuổi”, một người bán rau quả tên là Allen nói. Sau khi nghe kể lại rằng các nhà toán học phải mất bốn thế kỉ để tấn công vấn đề này và được hỏi anh thấy khó khăn như thế nào khi tìm cách xếp tốt nhất Allen đã thản nhiên trả lời: “Bạn chỉ việc đặt một quả lên trên đỉnh của những quả khác. Việc này chỉ mất khoảng 2 giây mà thôi”.

Sau mười năm nghiên cứu, một nghiên cứu sinh và tôi đã đưa ra chứng minh cho giả thuyết Kepler vào năm 1998. Chứng minh này dài ba trăm trang giấy. Nó dựa trên một khối lượng tính toán khổng lồ trên máy vi tính và phải mất nhiều tháng trời mới chạy xong.

2. Kiểm tra chứng minh

Trước khi bài báo được công bố một nhóm gồm mười hai nhà phản biện đã phải kiểm tra xem tôi có sai sót chỗ nào không. Sau nhiều tháng, họ vẫn không kiểm tra xong chứng minh, nhưng họ chắc đến 99% rằng chứng minh đúng. Tuy nhiên, họ quá mệt mỏi để tiếp tục công việc. Chứng minh cuối cùng đã được công bố sau tám năm mặc dù nó vẫn chưa được kiểm tra hoàn toàn đầy đủ.

Trong khi chờ đợi từ năm này qua năm khác, tôi bắt đầu nhận thấy rằng các nhà toán học đã mất bao nhiêu năm quý giá để kiểm tra các phép chứng minh. Tôi băn khoăn rằng chúng ta có nên thỏa mãn với các chứng minh được kiểm tra 99% hay không. Vậy phải chăng toán học luôn có nghĩa là phải chắc chắn hoàn toàn?

3. Chứng minh hình thức

Những năm tháng chờ đợi này đã làm tôi thay đổi hoàn toàn. Khi nghiên cứu việc kiểm tra chứng minh, tôi nhận thấy rằng các nhà logic học và các nhà khoa học máy tính đã phát triển các công cụ tự động để kiểm tra chứng minh. Những công cụ này là câu trả lời cho những mong mỏi của tôi. Một chứng minh được kiểm tra bằng máy tính theo cách này được gọi là chứng minh hình thức. Đối với những kết quả dài và phức tạp, một chức minh hình thức là đáng tin cậy trong khi những chứng minh thông thường thì không.

Để thực hiện một chứng minh hình thức, tất cả các tiền đề cơ sở của toán học được đưa vào trong máy tính. Tất cả các quy tắc logic cơ bản được lập trình trên máy tính. Sau đó máy tính sẽ xem xét từng bước logic để kiểm tra xem có sai sót nào không.

Ngày nay, những chứng minh cực kì phức tạp đều có thể được kiểm tra hình thức. Các nhà nghiên cứu đã chứng minh hình thức các định lý lớn như Định lý bốn màu. Định lý số nguyên tố, Định lý đường cong Jordan .

Tôi đã bắt đầu một dự án là Flyspeck để xây dựng một chứng minh hình thức cho giả thuyết Kepler. Từ Flyspeck của tôi sẽ lập trình cho máy tính để kiểm tra chứng minh mà nhóm mười hai người phản biện đã phải đầu hàng. Tôi mong rằng dự án này sẽ hoàn toàn trong vài năm. Hi vọng rằng dự án này sẽ làm thay đổi phương pháp kiểm tra các công trình trong tương lai.

4. Tại sao 99% lại không đủ tốt?

Nền kinh tế thế giới dựa trên sự chặt chẽ của toán học. Chúng ta tin vào vận tải hàng không và thương mại điện tử nhờ vào các chứng minh của các thuộc tính của chúng. Máy tính ngày càng xây dựng các chứng minh mà không cần sự trợ giúp của con người. Những sai sót về mặt toán học ngày càng có nguy cơ tiềm tàng cho nền kinh tế thế giới. Ví dụ như, cách đây một thập kỉ, một nhà toán học đã phát hiện ra rằng bộ vi xử lý Pentium của Intel chia số không chính xác. Lỗi chia này trong bộ vi xử lý đã làm Intel tiêu tốn mất 500 triệu đô la. Lỗi chia tiếp theo sẽ còn làm tiêu tốn nhiều hơn. Trong một bài báo gần đây, Shamir (chữ cái S trong thuật toán bảo mật RSA) cảnh báo về một sự cố mang tính giả thuyết về một lỗi toán học trong một bộ vi xử lí máy tính được sử dụng rộng rãi đặt việc bảo mật hệ thống thương mại điện tử toàn cầu vào tình thế mạo hiểm... Nếu một tổ chức phát hiện ra một lỗi toán học trong một bộ vi xử lí được sử dụng rộng rãi, thì phần mềm bảo mật của máy tính với bộ vi xử lí này sẽ bị phá hủy dễ dàng... Hàng triệu máy tính có thể bị tấn công đồng loạt.

Không có gì ngạc nhiên khi các công ti lớn trên thế giới ngày càng quan tâm đến các chứng minh hình thức. Geoges Gonthier, người xây dựng chứng minh hình thức của Định lí bốn màu đang làm việc tại Microsoft. John Harrison, người tạo ra phần mềm kiểm tra chứng minh mà tôi sử dụng đang làm việc tại Intel.

5. QED Manifesto

QED Manifesto khẳng định rằng tất cả các bài toán quan trọng nên được chuyển từ giấy sang máy tính. Để đảm bảo tính nguyên vẹn của tập hợp toán học này, tất cả các chứng minh phải chịu được lưu trữ như là các chứng minh hình thức. Đây là một dự án tham vọng và đòi hỏi sự hợp tác của các nhà toán học, các nhà logic học và các nhà khoa học máy tính trên tòan thế giới.

Dự án QED thực hiện cho toán học những gì mà dự án Flyspeck thực hiện cho chứng minh của giả thuyết Kepler. Dự án Flyspeck đại diện cho một phần nhỏ của dự án tổng thể QED.

6. Kết luận

Tôi mong muốn tổ chức một nhóm chứng minh định lí hình thức ở Việt Nam , hoàn thành dự án Flyspeck và để tiến tới dự án tổng thể QED. Tôi mong muốn tạo lập một mối liên kết lâu dài với cộng đồng toán học Việt Nam . Tôi xin mời các sinh viên và các nhà nghiên cứu tham gia vào dự án này.