Định lý Bốn Màu: Khi máy tính lần đầu vượt mặt các nhà toán học

Vào tháng 7 năm 1976, một bí ẩn toán học đã thách thức giới trí thức hơn một thế kỷ cuối cùng đã được giải quyết: định lý Bốn Màu. Điều đáng chú ý là hai tác giả Kenneth Appel và Wolfgang Haken đã phải nhờ đến một cộng sự không hề bình thường – một chiếc máy tính đảm nhiệm phần lớn khối lượng tính toán với 1.200 giờ xử lý và 10 tỷ quyết định.

Câu chuyện này nghe có vẻ quen thuộc với bất kỳ ai đang theo dõi làn sóng trí tuệ nhân tạo hiện nay, khi mà các mô hình học máy ngày càng đảm nhận những công việc mà con người từng cho là lãnh địa riêng.

Định lý Bốn Màu là gì?

Định lý Bốn Màu phát biểu rằng: không cần quá bốn màu để tô màu các vùng trên bất kỳ bản đồ nào sao cho hai vùng kề nhau không bao giờ có cùng một màu. Bài toán này được đặt ra từ năm 1852 và đã khiến nhiều thế hệ nhà toán học bế tắc suốt hơn 120 năm.

Để chứng minh định lý, Appel và Haken đã sử dụng máy tính để kiểm tra hàng nghìn cấu hình đặc biệt – một công việc bất khả thi nếu làm thủ công. Lập trình viên John Koch đã hỗ trợ hai ông phần việc thuật toán. Chính Appel và Haken sau đó thừa nhận rằng hệ thống "bắt đầu dạy chúng tôi những điều mà chúng tôi chưa từng mong đợi", và trong một số tác vụ trí tuệ nhất định, cỗ máy đã "vượt qua cả người tạo ra nó".

Minh họa định lý Bốn Màu trên bản đồ

Phản ứng của giới toán học: từ chấp nhận đến phủ nhận

Khác với hình dung về một cộng đồng khoa học đồng thuận, phản ứng của các nhà toán học vô cùng đa dạng – từ chấp nhận, phủ nhận cho đến thẳng thừng bác bỏ. Những con người tự hào về tính lý trí bỗng đối mặt với một "con quái vật toán học" mà họ coi như sự báng bổ.

"Chúa sẽ không bao giờ cho phép định lý được chứng minh bằng một phương pháp tồi tệ như vậy!" – Herbert Wilf, Đại học Pennsylvania

Một số người phản đối gay gắt khái niệm chứng minh toán học mà không cần lập luận toán học:

"Chứng minh hiện tại thực chất dựa vào một Nhà tiên tri, và tôi nói: đả đảo các Nhà tiên tri! Chúng không phải là toán học." – Paul Halmos, Đại học California, Santa Barbara

Một nhà toán học khác còn cho rằng nếu lời giải liên quan đến việc máy tính kiểm tra các trường hợp đặc biệt thì "lời giải đó hoàn toàn không thuộc về khoa học toán học". Thậm chí có người cáo buộc công trình là trò lừa đảo kiểu "Bộ quần áo mới của Hoàng đế" làm ô danh lịch sử toán học.

Một trưởng khoa toán còn từ chối cho Appel và Haken gặp các nghiên cứu sinh của mình, với lý do phương pháp của họ triệt tiêu động lực tìm kiếm một chứng minh thanh thoát và có thể kiểm chứng hơn.

Yếu tố tuổi tác và sự chia rẽ thế hệ

Điều thú vị là tuổi tác dường như là yếu tố quyết định mức độ chấp nhận chứng minh nhờ máy tính. Sau một buổi thuyết trình của con trai Haken, khán giả được cho là chia thành hai nhóm rõ rệt: "những người trên 40 tuổi không thể tin một chứng minh bằng máy tính là đúng, trong khi những người dưới 40 tuổi không thể tin một chứng minh chứa 700 trang tính toán thủ công lại đúng".

Sự chia rẽ trong giới toán học về chứng minh bằng máy tính

Từ hoài nghi đến công nhận

Chứng minh dần giành được sự hậu thuẫn từ những tên tuổi lớn. Nhà toán học huyền thoại Bill Tutte – người từng công khai nghi ngờ phương pháp này – cuối cùng đã chấp nhận và ăn mừng bằng một bài thơ:

Wolfgang Haken Đánh bại Kraken Một! Hai! Ba! Bốn! Ông tuyên bố: "Con quái vật không còn nữa."

Nhà toán học người Đức Heinrich Heesch chấp nhận chứng minh một cách miễn cưỡng, dù ông đã dành bốn thập kỷ cho bài toán và tạo ra chính những phương pháp thuật toán then chốt mà Appel và Haken sử dụng.

Tranh luận triết học: Chứng minh mà không cần lập luận?

Năm 1979, triết gia Thomas Tymoczko lập luận trên The Journal of Philosophy rằng một chứng minh không thể khảo sát hết bằng con người thì không phải là chứng minh toán học truyền thống:

"Không nhà toán học nào đã nhìn thấy một chứng minh của định lý Bốn Màu, cũng chưa ai thấy chứng minh rằng nó có chứng minh. Hơn nữa, rất khó có khả năng bất kỳ nhà toán học nào sẽ nhìn thấy."

Ted Swart phản bác lại quan điểm này, cho rằng "tôi coi chứng minh có máy tính hỗ trợ chỉ là một phần mở rộng của bút chì và giấy tờ". Ông cũng đặt câu hỏi về giả định bất khả ngộ của con người: "Con người mệt mỏi, sự tập trung lang thang, và họ rất dễ mắc đủ loại sai sót… Máy tính thì không mệt."

Tranh luận về chứng minh toán học có sự hỗ trợ của máy tính

Bài học cho thời đại AI

Câu chuyện năm 1976 mang tính tiên tri đáng kinh ngạc. Khi đó, giới toán học lo ngại rằng máy móc sẽ chiếm mất công việc trí tuệ của họ. Ngày nay, những tranh luận tương tự đang diễn ra xung quanh các mô hình ngôn ngữ lớn và trí tuệ nhân tạo tạo sinh.

Bill Tutte từng hình dung một nhà toán học tuyệt vọng kêu lên: "Tôi biết làm gì bây giờ?" Lời khuyên của ông vẫn còn nguyên giá trị:

"Hãy vững tâm. Bạn có thể tiếp tục theo đuổi cùng hướng nghiên cứu."

Và tất nhiên, ông cũng không quên một bài thơ:

Định lý Bốn Màu chỉ là phần nổi của tảng băng, là đầu nhọn của cái nêm và là tiếng chim cu gáy đầu tiên của mùa xuân.

Bài học rút ra rất rõ ràng: công nghệ mới luôn gây ra phản ứng dữ dội ban đầu, nhưng cuối cùng lại mở rộng giới hạn của những gì con người có thể làm được. Đối với độc giả Việt Nam theo dõi làn sóng AI hiện nay, câu chuyện định lý Bốn Màu là lời nhắc nhở rằng nỗi sợ hãi trước cái mới là chuyện bình thường, nhưng thích nghi và hợp tác với máy móc mới là con đường phía trước.