MỘT AI GIẢI ĐƯỢC CÂU ĐỐ TÔ MÀU

Hãy lấy một mạng lưới gồm các điểm nối với nhau bằng các đường — thứ mà các nhà toán học gọi là đồ thị. Giờ hãy tô màu các điểm sao cho hai điểm được nối bởi một đường không bao giờ cùng màu. Số màu nhỏ nhất làm được việc này là sắc số của đồ thị. Một trường hợp đặc biệt nổi tiếng là định lý bốn màu, được chứng minh năm 1977, với tiêu đề nói lên tất cả: “Every planar map is four colorable” (Mọi bản đồ phẳng đều tô được bằng bốn màu).

Canh bạc năm 1943 của Hadwiger

Năm 1943, Hadwiger đề xuất một quy tắc bao quát cho mọi đồ thị. Thu nhỏ một đồ thị bằng cách xóa điểm hoặc đường, và bằng cách gộp hai điểm được nối thành một. Kết quả được gọi là một đồ thị con thu gọn (minor). Hadwiger xét đồ thị đầy đủ lớn nhất — một cụm trong đó mọi điểm đều nối với mọi điểm khác — có thể thu được theo cách này, và phỏng đoán rằng số màu cần dùng không bao giờ vượt quá kích thước của cụm đó.

Bài báo gọi đây là bài toán “nằm trong số những bài toán lâu đời và căn bản nhất của lý thuyết đồ thị”. Nó mới chỉ được chứng minh cho các trường hợp nhỏ: với cụm có tối đa năm điểm, nó hóa ra tương đương với định lý bốn màu hoặc quy về được định lý đó. Từ sáu trở lên, nó vẫn bỏ ngỏ.

Tiến lại gần, từng logarit một

Vì phát biểu chính xác quá khó, các nhà nghiên cứu tìm cách chặn số màu bằng một hàm nào đó của kích thước cụm, tăng càng chậm càng tốt. Bài báo kể lại những bước tiến. Trong nhiều thập kỷ, cận tốt nhất tăng nhanh hơn tỷ lệ thuận một chút — thêm một thừa số chứa căn bậc hai của một logarit. Vài năm trước, Norin, Postle và Song đã phá vỡ rào cản đó. Delcourt và Postle sau đó cải thiện thêm và, điều then chốt, chỉ ra rằng chỉ cần xử lý những đồ thị khá nhỏ là đủ. Liu và Luo đẩy thừa số dư xuống còn một logarit lặp ba lần.

Điểm đến tự nhiên là phỏng đoán Hadwiger tuyến tính: một bội số cố định của kích thước cụm luôn là đủ. Đó là điều mà Sergey Norin, thuộc Đại học McGill ở Montreal, và Raphael Steiner, thuộc ETH Zurich, giờ đây tuyên bố đã chứng minh.

Phần việc của cỗ máy

Các tác giả nói rõ: chứng minh được tìm ra bởi GPT-6 Astra, một mô hình của OpenAI, theo chỉ dẫn của họ. Đầu tiên, họ yêu cầu nó chứng minh trường hợp đồ thị rất dày, mà họ tin là mảnh ghép còn thiếu. Nó đã thành công, họ viết, “chỉ sau vài giờ và một chút động viên”. Khi được yêu cầu làm tường minh một sự phụ thuộc, nó bao quát được các đồ thị đến một kích thước nhất định — nhưng chưa hẳn đủ phạm vi cần thiết. Họ bèn yêu cầu nó một ý tưởng độc đáo để lấp khoảng trống, và điều đó sinh ra bước “tự khuếch đại” (bootstrap) của chứng minh cuối cùng. Theo họ, hầu như không ý tưởng chứng minh cụ thể nào của chính các tác giả còn sót lại, ngoài một gợi ý về phép co.

Phần viết là của con người. Một mô hình khác của OpenAI hỗ trợ việc soát lỗi và danh mục tài liệu tham khảo. Các tác giả cho biết Codex của OpenAI đã tạo ra một phiên bản hình thức, có thể kiểm tra bằng máy, của toàn bộ chứng minh trong trợ lý chứng minh Lean, được đăng trực tuyến cùng một bản nháp đầu tiên do AI viết. Họ chịu hoàn toàn trách nhiệm về phần toán học.

Bên trong chứng minh

Lập luận gồm hai nửa:

1. Đồ thị nhỏ, ít màu. Với những đồ thị không lớn hơn giới hạn cụm là bao, các tác giả chỉ ra rằng khoảng bốn lần kích thước cụm là đủ. Điểm xuất phát là một kết quả năm 1998 của Reed và Seymour: một dạng tô màu nới lỏng, “phân số”, đã tuân theo quy tắc tuyến tính với thừa số hai. Công trình mới biến các cách tô màu phân số thành cách tô màu thật bằng cách thêm vài đường vào đồ thị và tìm những cặp ghép khổng lồ trong một cấu trúc phụ trợ.
2. Tự khuếch đại. Một lập luận thứ hai mở rộng phạm vi kích thước đồ thị được bao quát thêm một thừa số bốn phần ba ở số mũ sau mỗi bước, đổi lại một hằng số lớn hơn. Mười bước đưa phạm vi từ một phần ba lên khoảng 5,92, vượt ngưỡng 5 mà phép quy giản Delcourt-Postle đòi hỏi. Nửa này dùng một mẹo cũ của Gyárfás, mà theo các tác giả chưa từng được áp dụng cho bài toán này.

Các tác giả mô tả chứng minh như được xây từ những công cụ đã biết — “nằm trong bao lồi của các kết quả hiện có”, nhưng không nằm trên một cạnh hiển nhiên của nó.

Những gì còn bỏ ngỏ

Hằng số thì khổng lồ: một ước lượng thô cho khoảng 10¹⁰⁰. Các tác giả thấy có chỗ để hạ nó xuống dưới 10¹⁰, nhưng nghĩ rằng để đạt tới, chẳng hạn, 100 thì sẽ cần những ý tưởng mới. Phỏng đoán chính xác của Hadwiger thì chưa bị đụng tới: “Chúng tôi chưa quyết định được”, họ viết. Bài báo là một bản tiền ấn phẩm; 41 trang toán học mới giờ đây sẽ phải đối mặt với sự soi xét của các chuyên gia khác.