AI chứng minh trần 63 nước chiếu: bài toán cờ vua 58 năm và phần còn bỏ ngỏ

Trong làng cờ vua, có một góc không ai vỗ tay. Không đồng hồ, không khán đài, không Elo. Chỉ có một bàn cờ đặt lặng lẽ và một câu hỏi mà giới soạn thế cờ theo đuổi hơn nửa thế kỷ: trong một thế cờ duy nhất, tối đa có bao nhiêu nước đi hợp lệ mà tất cả đều là nước chiếu? Norbert Ringeltaube, một nhà soạn thế cờ kỳ cựu, từng giữ kỷ lục với 60 nước chiếu. Kỷ lục ấy không lên bảng tin thể thao; nó nằm trong những tập san chuyên môn, nơi người ta tranh luận bằng ký hiệu và sơ đồ thế cờ. Tôi từng nghĩ chẳng gì thay đổi được cái trần đó. Rồi ngày 13/10, một hệ thống AI mang tên Double Agent công bố nó tìm ra và chứng minh được con số 63 — và quan trọng hơn, chứng minh rằng không thế cờ nào vượt qua được 63. Bối cảnh Phải tách hai bài toán, vì trộn chúng lại là cách nhanh nhất để hiểu sai câu chuyện. Bài toán thứ nhất là số nước chiếu tối đa trong một thế cờ duy nhất. Kỷ lục cũ là 60 của Ringeltaube; kết quả mới là 63. Đây là một kết quả khép kín: vừa tồn tại một thế cờ đạt 63, vừa chứng minh không thể vượt 63. Bài toán thứ hai là chuỗi nước chiếu liên tiếp dài nhất. Nhà soạn thế cờ Alexey Khanyan từng dựng một chuỗi 54 nước vào năm 2026. Double Agent công bố một cận trên 364, nhưng đây chỉ là cận trên, chưa phải giá trị lớn nhất chính xác. Bài toán thứ hai vẫn còn mở. Sự khác biệt ấy gần như không xuất hiện trong các tiêu đề. Điều kiện hợp lệ là chỗ dễ bị bỏ qua nhất. Thế cờ kỷ lục phải có thể phát sinh từ một ván cờ hợp lệ, không phải một cấu trúc cổ tích. Bên đi phải có ít nhất một nước hợp lệ, và tất cả đều là nước chiếu. Không có những ràng buộc ấy, người ta xếp quân tùy ý và con số trở nên vô nghĩa. Nói cho rõ, chủ thể ở đây là toán tổ hợp trên bàn cờ, chứ chẳng phải một ván cờ vua thi đấu nào. Không có kỳ thủ nào, không có ván nào, không có đồng hồ nào. Trong giới soạn thế cờ, mỗi kỷ lục là kết quả của nhiều năm mò mẫm. Người ta không thi đấu với nhau qua các ván, mà qua những sơ đồ đăng trên tạp chí, chờ người khác tìm ra lỗi. Đây là một cộng đồng nhỏ, kín, và cực kỳ khắt khe. Một kỷ lục chỉ được công nhận khi không ai bác bỏ được nó. Tôi nhớ những năm ngồi bình luận cờ vua cho VTC. Suốt 19 năm ấy, tôi học được một điều: người xem chỉ nhớ nước đi quyết định, nhưng người trong nghề nhớ cách người ta đi tới nước ấy. Câu chuyện của Double Agent cũng vậy. Nó không nằm ở ánh đèn, mà nằm ở một góc tối của bàn cờ, nơi chỉ vài trăm người trên thế giới thật sự quan tâm. Phân tích Điểm đáng giá nhất nằm ở phương pháp, không nằm ở con số. Nhóm nghiên cứu nói rằng liệt kê thô là bất khả thi: không gian thế cờ quá lớn để quét hết. Thay vào đó, họ đi theo một đường ống bốn bước. Trước tiên, chứng minh các tính chất hình học và cấu trúc của những thế cờ toàn chiếu. Sau đó, hình thức hóa chúng trong Lean 4, một trợ lý chứng minh mà máy có thể kiểm tra. Tiếp theo, quy phần còn lại về một bài toán SAT. Cuối cùng, để máy kiểm chứng toàn bộ chứng minh. Theo bài công bố, đây là kết quả cực trị đầu tiên trong nhánh soạn thế cờ này được máy xác minh. Nói cách khác, thành tựu thật sự là quy trình. Trước đây, kỷ lục do con người lập ra dựa trên trực giác và kinh nghiệm dựng thế cờ. Giờ đây, một hệ thống kết hợp tìm kiếm, logic toán và chứng minh máy kiểm tra được đã tham gia. Con số đi từ 60 lên 63, chỉ ba đơn vị. Nhưng ba đơn vị ấy đến từ một cách làm hoàn toàn khác. Để dựng được một thế cờ đạt 63 nước chiếu, người ta gần như phải ép mật độ quân lên mức tối đa, đồng thời dùng ghim quân và chặn đường để vô hiệu hóa mọi nước không chiếu. Đây là suy luận của tôi từ mô tả "sắp xếp chặt", ghim quân và kiểm soát ô, chứ bài gốc không nói thẳng. Nhưng nó khớp với lý do vì sao liệt kê thô bất khả thi: càng ép mật độ, không gian tìm kiếm càng phình ra theo cấp số nhân. Tôi đã theo dõi rất nhiều ván cờ đỉnh cao, và tôi biết một điều: đằng sau mỗi nước đi tưởng như khô khan là một quyết định của con người. Ở đây thì khác. Không có con người ngồi sau bàn cờ. Có một thuật toán, một trợ lý chứng minh, và một bài toán SAT. Vậy mà tôi vẫn thấy nó gợi lên đúng cái cảm giác cũ: một người ngồi trước bàn cờ, nuốt nước bọt, rồi đi một nước mà không ai lường trước. Bàn cờ quê nhà không có khán đài, nhưng mỗi thế cờ vẫn là cả một trời ký ức ùa về. Cũng cần nói rõ một điểm về độ tin cậy. Một số nhận định trong công bố mang tính ý kiến, không phải chứng minh. Chẳng hạn, ý cho rằng thêm quân hay thêm sức tấn công "có thể không cải thiện kết quả" được trình bày như một phỏng đoán. Người đọc tin này nên phân biệt rạch ròi giữa cái đã được chứng minh và cái chỉ được suy đoán. Với tôi, đó là kỷ luật tối thiểu khi đứng trước một tiêu đề đẹp. Góc phản trực giác Có một nghịch lý đáng chú ý trong cách câu chuyện này được kể lại. Tiêu đề "AI giải một bài toán cờ vua 58 năm tuổi" dễ khiến người đọc nghĩ cờ vua đã bị "giải" theo một nghĩa rộng nào đó. Bản chất hẹp hơn nhiều: một định lý cực trị nhỏ đã được chứng minh, còn một câu hỏi khác vẫn để ngỏ với con số 364 chỉ là cận trên. Khoảng cách giữa tiêu đề và bản chất là một khoảng cách lớn. Rủi ro thứ hai là nguồn gốc của sự xác minh. Chứng minh được cho là "máy kiểm tra", nhưng do chính nhóm nghiên cứu thực hiện. Không có kiểm toán độc lập nào được báo cáo. Trong giới phương pháp hình thức, đây là điểm yếu kinh điển: máy kiểm tra được không đồng nghĩa với đúng, bởi một lỗi mã hóa trong bước quy về SAT có thể làm sai toàn bộ cận trên. Tôi không nói kết quả sai. Tôi nói nó chưa được đối chứng bởi bên thứ ba. Rủi ro thứ ba là độ mờ của nguồn tin. Bài gốc không nêu rõ cơ quan công bố, và phần lớn dữ kiện không có nguồn dẫn. Khi một con số đi xa hơn bản chất của nó, nó thường đi kèm một tiêu đề đẹp hơn sự thật. Đây là bài học tôi rút ra sau nhiều năm làm tài liệu: tín hiệu thật thường lặng lẽ, còn tiếng ồn thì luôn to. Đọng lại Điều tôi muốn giữ lại không nằm ở con số 63, mà ở ý tưởng rằng một góc bàn cờ tưởng như bị lãng quên đã trở thành nơi thử nghiệm chuẩn mực chứng minh mới. Nếu cộng đồng soạn thế cờ dần chấp nhận quy trình xác minh bằng máy cho các tuyên bố cực trị, thì giá trị thật của ngày 13/10 không nằm ở ba nước chiếu thêm, mà ở một thói quen mới: không tin vào con số đẹp, chỉ tin vào chứng minh kiểm tra được. Và biết đâu, khi bài toán 364 nước kia được khép lại, người ta sẽ nhớ tới nó như một khởi đầu, chứ không phải một kết thúc.