Định lý bốn màu khẳng định chỉ cần bốn màu là đủ tô mọi bản đồ trên mặt phẳng, sao cho hai vùng có chung một đoạn biên luôn khác màu. Kenneth Appel và Wolfgang Haken chứng minh nó năm một nghìn chín trăm bảy mươi sáu, với một phần lớn công việc kiểm tra giao cho máy tính, điều chưa từng có với một định lý lớn.
Chào bạn, đây là Nhà Học Thuật. Bài toán này một em học sinh cũng hiểu được, vậy mà mất hơn một thế kỷ mới giải xong, và cách giải lại làm giới toán học chia rẽ. Tập này mình kể vì sao nó khó, và vì sao câu hỏi một máy tính có được phép chứng minh hay không lại quan trọng.
Một câu hỏi từ việc tô bản đồ
Giữa thế kỷ mười chín, một người Anh trẻ tên Francis Guthrie, khi tô bản đồ các hạt của nước Anh, để ý rằng bốn màu dường như luôn đủ. Câu hỏi được chuyển tới nhà toán học Augustus De Morgan, và ông lan truyền nó trong giới toán học.
Dễ thấy ba màu là không đủ: vẽ bốn vùng mà vùng nào cũng chạm ba vùng còn lại là xong. Cũng dễ thấy năm vùng đôi một chạm nhau là không vẽ được trên mặt phẳng. Nhưng từ đó không suy ra được bốn màu luôn đủ, vì cái khó nằm ở những bản đồ lớn với cấu trúc rối rắm.
Lưu ý là mỗi vùng phải liền một khối, và hai vùng chỉ chạm nhau ở một điểm thì không tính là chung biên.
Bài toán thực ra không phục vụ người vẽ bản đồ. Họ hiếm khi bận tâm tới số màu tối thiểu. Đây là một câu hỏi thuần tuý về cấu trúc của mặt phẳng.
Chứng minh sai sống được mười một năm
Năm một nghìn tám trăm bảy mươi chín, luật sư kiêm nhà toán học Alfred Kempe công bố một chứng minh, được chấp nhận rộng rãi. Mười một năm sau, Percy Heawood phát hiện lỗ hổng không vá được.
Nhưng chứng minh sai của Kempe để lại hai ý tưởng quý. Một là kỹ thuật đổi màu theo chuỗi, sau này gọi là chuỗi Kempe. Hai là chiến lược: chỉ ra rằng mọi bản đồ đều phải chứa ít nhất một cấu hình trong một danh sách không thể tránh, và mỗi cấu hình trong danh sách ấy đều có thể rút gọn được.
Heawood dùng chính các ý tưởng đó để chứng minh năm màu luôn đủ. Khoảng cách từ năm xuống bốn tưởng nhỏ, hoá ra mất gần chín mươi năm nữa.
Câu chuyện Kempe là lời nhắc rằng cả giới chuyên môn có thể tin vào một chứng minh sai trong nhiều năm. Bình duyệt không phải là bảo đảm tuyệt đối.
Appel, Haken và hàng nghìn cấu hình
Trong thế kỷ hai mươi, người ta hiểu rằng chiến lược Kempe có thể thành công, nhưng danh sách cấu hình không thể tránh phải rất dài, có thể hàng nghìn cái, và mỗi cái phải được kiểm tra khả năng rút gọn qua vô số cách tô.
Ở Đại học Illinois, Kenneth Appel và Wolfgang Haken, cùng sự giúp sức của John Koch về lập trình, kết hợp phân tích bằng tay với tính toán bằng máy. Danh sách cuối cùng của họ có gần hai nghìn cấu hình, và việc kiểm tra tiêu tốn hơn một nghìn giờ máy tính thời ấy.
Năm một nghìn chín trăm bảy mươi sáu, họ công bố kết quả. Theo một giai thoại hay được kể, khoa toán của trường còn đóng dấu bưu điện dòng chữ bốn màu là đủ lên thư gửi đi.
Phần làm bằng tay của chứng minh cũng dài và phức tạp, và trong những năm sau đã có vài lỗi nhỏ được phát hiện và sửa. Điều đó càng làm nhiều người băn khoăn.
Chứng minh mà không ai đọc hết được có phải là chứng minh?
Theo quan niệm truyền thống, chứng minh là một chuỗi lập luận mà một người có năng lực đọc từ đầu tới cuối và tự thấy là đúng. Chứng minh của Appel và Haken không thoả điều đó: không con người nào kiểm tra từng trường hợp máy đã chạy.
Nhà triết học Thomas Tymoczko lập luận rằng định lý bốn màu đưa một yếu tố thực nghiệm vào toán học. Ta tin nó gần giống cách ta tin một kết quả thí nghiệm, dựa vào độ tin cậy của máy móc và chương trình.
Phía bảo vệ đáp lại rằng con người cũng mắc lỗi, nhiều khi còn hơn máy, và những chứng minh dài hàng trăm trang bằng tay cũng chẳng mấy ai đọc trọn. Cái cần là quy trình kiểm tra đáng tin, dù người hay máy làm.
Đây không chỉ là chuyện thẩm mỹ. Nó chạm vào câu hỏi tri thức toán học có đặc biệt chắc chắn hơn mọi tri thức khác hay không.
Từ nghi ngờ đến kiểm chứng hình thức
Giữa thập niên chín mươi, nhóm của Neil Robertson, Daniel Sanders, Paul Seymour và Robin Thomas đưa ra một chứng minh gọn hơn, với danh sách cấu hình ngắn hơn và mã nguồn công khai cho ai cũng chạy lại được.
Năm hai nghìn không trăm linh năm, Georges Gonthier cùng cộng sự hoàn tất việc kiểm chứng toàn bộ chứng minh trong một trợ lý chứng minh, tức phần mềm kiểm tra từng bước suy luận theo luật logic chặt chẽ. Lúc này, cả phần trước kia làm bằng tay cũng được máy soát.
Ngày nay, kiểm chứng hình thức đang lan sang nhiều mảng toán học khác, và đã có những dự án cộng đồng lớn chuyển các kết quả hiện đại sang ngôn ngữ máy kiểm tra được.
Câu hỏi năm nào gây chia rẽ giờ trở thành một hướng nghiên cứu sôi động. Có lẽ tương lai của chứng minh là con người nghĩ ra ý tưởng, còn máy giữ cho mọi bước đều thật sự đúng.
Câu hỏi thường gặp
Trên mặt hình khác mặt phẳng thì cần bao nhiêu màu?
Tuỳ hình dạng mặt. Trên mặt chiếc phao bơi, cần tới bảy màu cho một số bản đồ. Điều thú vị là các mặt phức tạp này được giải quyết từ trước, còn mặt phẳng lại khó nhất.
Lý thuyết đồ thị liên quan gì tới bài toán bốn màu?
Có thể thay mỗi vùng bằng một điểm, nối hai điểm khi hai vùng chung biên. Bài toán thành tô màu các điểm sao cho hai điểm nối nhau khác màu. Cách nhìn này giúp bài toán được nghiên cứu bằng công cụ của lý thuyết đồ thị.
Trợ lý chứng minh là gì?
Đó là phần mềm cho phép viết chứng minh dưới dạng mà máy kiểm tra được từng bước theo quy tắc logic. Người viết vẫn phải nghĩ ra lập luận, máy chỉ bảo đảm không có bước nào sai.
Có ai tìm ra chứng minh bốn màu ngắn không cần máy chưa?
Đến nay chưa có chứng minh nào được chấp nhận mà không dựa vào máy tính. Đây vẫn là một câu hỏi mở thú vị với nhiều nhà toán học.
Định lý bốn màu có ứng dụng thực tế không?
Bản thân định lý ít được dùng trực tiếp, nhưng các bài toán tô màu đồ thị nói chung xuất hiện trong xếp lịch thi, phân tần số sóng vô tuyến và cấp phát tài nguyên máy tính.
