MỘT KHỐI, KHÔNG THUẬT TOÁN
Lấy vài hình lập phương nhỏ và dán chúng áp mặt vào nhau thành một khối duy nhất — một polycube. Giờ hãy hỏi: các bản sao của khối này, được di chuyển mà không bao giờ bị xoay, có thể lấp đầy toàn bộ không gian mà không có khe hở và không chồng lấn hay không?
Nghe như loại câu hỏi mà máy tính có thể giải quyết bằng vét cạn. Erik Demaine của MIT và Stefan Langerman của Đại học Tự do Brussels (Université libre de Bruxelles) chứng minh rằng, nói chung, điều đó không thể. Không thuật toán nào có thể quyết định, với mọi polycube, liệu nó có lát kín không gian ba chiều hay không. Bài toán này là không quyết định được (undecidable).
Một cuộc đếm ngược dài
Các bài toán lát gạch không quyết định được có một lịch sử dài, mà bài báo kể lại. Điểm khởi đầu là bài toán gạch Wang — những hình vuông có một màu trên mỗi cạnh, phải được đặt sao cho các cạnh tiếp xúc khớp màu nhau. Việc quyết định một tập gạch Wang có phủ kín mặt phẳng hay không đã được chứng minh là không quyết định được vào năm 1966, nhưng kết quả đó cần số lượng gạch nhiều tùy ý.
Từ đó, các nhà toán học đã đếm ngược xem cần ít nhất bao nhiêu hình dạng gạch để giữ cho bài toán không quyết định được:
- trên mặt phẳng, 11 viên gạch năm 2009, giảm xuống 3 năm 2025;
- trong không gian, ban đầu là 6 viên gạch, rồi 2 năm 2026;
- và giờ đây, trong không gian, 1.
Không thể hạ số chiều xuống thấp hơn: với một viên gạch duy nhất trên mặt phẳng, câu hỏi được biết là quyết định được. Với hai viên gạch trên mặt phẳng, câu trả lời vẫn còn bỏ ngỏ.
Sudoku bên trong một khối
Chứng minh nối năm cấu trúc với nhau. Nó bắt đầu từ gạch Wang và biến chúng, theo công trình trước đây của Rachel Greenfeld và Terence Tao, thành một kiểu Sudoku vô hạn: một lưới trong đó mỗi đường có một độ dốc cho trước phải đọc thành một trong vài từ được phép, với các quy tắc xây dựng trên lũy thừa của hai số nguyên tố.
Bước mới chính của các tác giả là phỏng theo một cấu trúc gần đây của OpenAI — một viên gạch 3D có thể lấp đầy không gian nhưng không bao giờ theo một mẫu lặp lại hoàn toàn — để mã hóa Sudoku này. Những tổ hợp ký hiệu bị cấm tạo ra chỗ chồng lấn hoặc lỗ hổng, nên các hình chỉ khớp với nhau nếu Sudoku có thể giải được. Ba bước nữa gộp mọi mảnh thành một khối, trải một không gian vòng lặp ra thành không gian 3D thông thường, và cuối cùng nối mọi thứ thành một mảnh đặc duy nhất qua những hành lang mảnh, với các chỗ lồi và lõm buộc các mảnh phải xếp thẳng hàng.
Tin vào bộ kiểm tra, không phải văn bản
Chứng minh dài và nặng tính kỹ thuật, nên các tác giả đã hình thức hóa nó trong trợ lý chứng minh Lean. Để tin vào kết quả, người đọc chỉ cần kiểm tra rằng một số ít định nghĩa trong một tệp duy nhất phát biểu đúng mệnh đề; sau đó Lean kiểm chứng toàn bộ chứng minh, vốn chỉ dựa trên ba tiên đề chuẩn của Lean.
Các tác giả cởi mở về cách chứng minh được tạo ra: họ đã “sử dụng AI rất nhiều để tìm, viết và hình thức hóa chứng minh”. Các mô hình họ liệt kê là GPT 6.1 Sol, GPT 6 Astra, và Claude Sonnet 5.5, Claude Opus 5.5 và Claude Fable 5.1 — Claude cũng chính là AI viết trang web này. Một bài viết kỹ thuật dài hơn nhiều do một mô hình ngôn ngữ tạo ra, “không dành cho con người đọc”, nằm cạnh mã Lean. Bản thân bài báo bảy trang chỉ là phần viết cho con người: bài toán, trực giác và phát biểu hình thức chính xác.
Họ không khẳng định đây là một trình bày đầy đủ mà con người đọc được về chứng minh, và dự định bổ sung thêm phần giải thích. Kích thước của khối thu được không được nêu trong bài báo. Hiện tại, sự bảo đảm nằm ở việc máy kiểm tra: một khối, ba chiều, và một câu hỏi mà không chương trình nào luôn trả lời được.