Định lý bốn màu nói rằng mọi bản đồ vẽ trên mặt phẳng đều tô được bằng tối đa bốn màu sao cho hai vùng chung đường biên không cùng màu. Câu hỏi được đặt ra năm 1852, và phải đến năm 1976 mới được Kenneth Appel và Wolfgang Haken chứng minh — lần đầu tiên trong lịch sử, một định lý lớn được chứng minh nhờ máy tính kiểm tra hàng nghìn trường hợp.
Câu hỏi của một sinh viên tô bản đồ
Năm 1852, Francis Guthrie, một sinh viên người Anh, đang tô bản đồ các hạt (county) của nước Anh. Anh để ý rằng chỉ cần bốn màu là đủ để hai hạt cạnh nhau luôn khác màu. Liệu điều đó có đúng với mọi bản đồ? Guthrie hỏi em trai Frederick, và Frederick mang câu hỏi đến thầy mình, nhà toán học Augustus De Morgan. De Morgan không giải được, nhưng viết thư kể cho nhà toán học William Rowan Hamilton. Bức thư ngày 23 tháng 10 năm 1852 ấy là ghi chép sớm nhất còn lại về bài toán.
Luật chơi chính xác
- Hai vùng chung một đoạn biên phải khác màu.
- Hai vùng chỉ chạm nhau ở một điểm (như các ô đen trắng trên bàn cờ) được phép cùng màu.
- Mỗi vùng là một khối liền. Nếu một nước có lãnh thổ tách rời mà bắt buộc mọi phần cùng màu, định lý không còn đảm bảo.
- Bản đồ vẽ trên mặt phẳng hoặc mặt cầu (như quả địa cầu).
Vì sao ba màu không đủ
Dễ thấy cần ít nhất bốn màu: vẽ một vùng ở giữa, bao quanh bởi ba vùng, mỗi vùng chạm cả hai vùng còn lại và chạm vùng giữa. Bốn vùng đôi một kề nhau → cần bốn màu. Ví dụ đời thường: một nước bị bao quanh bởi ba nước láng giềng nối thành vòng. Cái khó là chứng minh không bao giờ cần đến màu thứ năm.
Một thế kỷ chứng minh sai và gần đúng
| Năm | Sự kiện |
|---|---|
| 1852 | Francis Guthrie đặt câu hỏi; De Morgan viết thư cho Hamilton |
| 1879 | Alfred Kempe công bố một chứng minh, được tin là đúng suốt 11 năm |
| 1880 | Peter Guthrie Tait đưa thêm một chứng minh khác, sau cũng bị phát hiện sai |
| 1890 | Percy Heawood chỉ ra lỗ hổng trong chứng minh của Kempe, và dùng chính ý tưởng ấy chứng minh được "năm màu là đủ" |
| Đầu – giữa thế kỷ 20 | Nhiều nhà toán học thu hẹp bài toán, chứng minh đúng cho bản đồ ít vùng |
| 1976 | Appel và Haken (Đại học Illinois) chứng minh bằng máy tính |
| 1996 | Robertson, Sanders, Seymour, Thomas đưa ra chứng minh gọn hơn, vẫn cần máy tính |
| 2005 | Georges Gonthier kiểm tra toàn bộ chứng minh bằng phần mềm kiểm chứng hình thức |
Câu chuyện của Kempe đáng nhớ: một chứng minh sai được giới toán học chấp nhận hơn một thập kỷ. Nhưng ý tưởng của ông — đổi màu theo từng "chuỗi" vùng hai màu xen kẽ, nay gọi là chuỗi Kempe — lại trở thành công cụ trung tâm của chứng minh đúng gần một trăm năm sau.
Máy tính đã làm gì
Ý tưởng chứng minh của Appel và Haken có thể nói gọn thế này. Giả sử có một bản đồ "tệ nhất" cần năm màu, và là bản đồ nhỏ nhất như vậy. Họ chỉ ra rằng bản đồ nào cũng phải chứa ít nhất một trong một danh sách các mẫu hình nhỏ (cấu hình) — danh sách này có gần hai nghìn mẫu. Rồi họ chứng minh rằng mẫu nào trong danh sách cũng "rút gọn được": nếu bản đồ nhỏ hơn tô được bốn màu, thì gắn mẫu đó vào vẫn tô được bốn màu. Mâu thuẫn — vậy bản đồ tệ nhất không tồn tại.
Phần kiểm tra từng mẫu quá nhiều để làm bằng tay, nên họ cho máy tính chạy, mất khoảng hơn một nghìn giờ máy thời đó.
Cuộc tranh luận: máy tính chứng minh có tính không?
Năm 1976, nhiều nhà toán học không vui. Chứng minh truyền thống là thứ một người có thể đọc và kiểm từng dòng. Chứng minh của Appel và Haken thì không ai đọc hết được phần máy tính làm. Nếu chương trình có lỗi thì sao? Cuộc tranh luận kéo dài nhiều năm, và góp phần thay đổi cách giới toán học nghĩ về chứng minh.
Đến năm 2005, khi Gonthier dùng một phần mềm kiểm chứng hình thức để kiểm toàn bộ lập luận — từng bước logic được máy xác nhận — phần lớn nghi ngờ đã lắng xuống. Ngày nay, định lý bốn màu được chấp nhận rộng rãi là đúng.
Người làm bản đồ có thật sự cần bốn màu?
Thú vị là người vẽ bản đồ ít khi quan tâm định lý này. Bản đồ thật thường có thêm điều kiện: biển phải màu xanh, nước có lãnh thổ tách rời phải cùng màu, và người ta muốn nhiều màu cho đẹp, dễ phân biệt. Định lý bốn màu là bài toán toán học thuần tuý được gợi ý từ bản đồ, hơn là một công cụ của nghề vẽ bản đồ.
Ứng dụng thật của bài toán tô màu nằm ở chỗ khác: xếp lịch, chia tần số sóng, phân ca — những bài toán mà "màu" là khung giờ hay kênh sóng.
Góc nhìn hôm nay: tự tô bản đồ Việt Nam
In một bản đồ các tỉnh thành Việt Nam không có màu. Thử tô bằng bốn màu, sao cho hai tỉnh chung đường ranh giới khác màu. Bắt đầu từ vùng có nhiều láng giềng nhất, để những tỉnh ven biển, ít láng giềng lại sau. Đếm xem có tỉnh nào buộc phải dùng màu thứ tư không. Rồi thử với ba màu — bạn sẽ thấy ở đâu đó trên bản đồ có một tỉnh bị bao bởi một vòng láng giềng số lẻ, và ba màu không còn đủ. Đó chính là trái tim của bài toán mà người ta mất 124 năm để giải.
Câu hỏi thường gặp
Định lý bốn màu là gì?
Là định lý nói rằng mọi bản đồ trên mặt phẳng đều tô được bằng tối đa bốn màu sao cho hai vùng chung đường biên không cùng màu. Hai vùng chỉ chạm nhau ở một điểm được phép cùng màu.
Ai chứng minh định lý bốn màu?
Kenneth Appel và Wolfgang Haken ở Đại học Illinois chứng minh năm 1976 với sự trợ giúp của máy tính. Năm 1996 có chứng minh gọn hơn, và năm 2005 toàn bộ được kiểm bằng phần mềm kiểm chứng hình thức.
Vì sao định lý bốn màu gây tranh cãi?
Vì đây là định lý lớn đầu tiên mà phần kiểm tra quá dài để con người đọc hết, phải nhờ máy tính chạy hơn một nghìn giờ. Nhiều người lo ngại chương trình có thể sai.
Ba màu có đủ để tô mọi bản đồ không?
Không. Một vùng bị bao quanh bởi ba vùng nối thành vòng tạo ra bốn vùng đôi một kề nhau, cần bốn màu.
Ai đặt ra bài toán bốn màu?
Francis Guthrie, một sinh viên người Anh, năm 1852 khi đang tô bản đồ các hạt của nước Anh. Câu hỏi được truyền đến Augustus De Morgan và ghi lại trong thư gửi Hamilton.