Chứng minh tối ưu cách xếp 11 hình vuông nhờ trợ giúp của AI

Một dự án mã nguồn mở vừa công bố chứng minh hình thức hoàn chỉnh cho bài toán xếp 11 hình vuông vào một hình vuông lớn nhất với cạnh nhỏ nhất có thể. Điểm đáng chú ý là chứng minh này được hỗ trợ bởi AI và đã vượt qua toàn bộ quá trình kiểm tra tự động.

Toàn bộ 7.920 mô-đun Lean cục bộ đều được chấp nhận, và báo cáo kiểm toán cuối cùng ghi nhận không có tiên đề nào bị thừa nhận (zero admissions) — một tiêu chuẩn khắt khe trong lĩnh vực chứng minh hình thức.

Bài toán xếp hình vuông là gì?

Bài toán xếp 11 hình vuông thuộc nhóm bài toán tối ưu hóa hình học cổ điển: cho 11 hình vuông nhỏ có thể xoay hướng tùy ý, tìm cách sắp xếp chúng gọn nhất trong một hình vuông bao ngoài sao cho cạnh của hình vuông lớn là nhỏ nhất.

Đây là dạng bài toán tưởng đơn giản nhưng cực kỳ phức tạp khi cần chứng minh tính tối ưu — tức là chứng minh không tồn tại cách xếp nào tốt hơn. Máy tính có thể tìm ra một cách xếp tốt, nhưng để chứng minh nó là tốt nhất thì cần lập luận toán học chặt chẽ.

Kết quả đạt được

Theo công bố, độ dài cạnh tối ưu được xác định bằng công thức:

T = (6u + 4) / (1 + 2u − u²)

Trong đó u là nghiệm duy nhất trong khoảng (9/25, 37/100) của phương trình bậc tám:

5u⁸ − 10u⁷ − 2u⁶ + 14u⁵ + 12u⁴ − 6u³ + 2u² + 2u − 1 = 0

Cách xếp này đạt giá trị xấp xỉ 3,8770835900228141773. Mô hình cho phép các hình vuông xoay hướng tùy ý, tiếp xúc hợp lệ với biên, và có phần trong rời nhau.

Vai trò của AI và Lean

Dự án sử dụng Lean 4 — một trợ lý chứng minh hình thức mạnh mẽ — kết hợp với các chứng chỉ số học gốc. Một số phép kiểm tra số học đắt đỏ được thực hiện bằng native_decide, trong khi phần hình học, tính đúng đắn của bộ kiểm tra và việc lắp ghép chứng minh vẫn dùng các chứng minh Lean thông thường.

Điều này có nghĩa là định lý cuối cùng đặt niềm tin vào nhân Lean và trình biên dịch gốc — đây không phải là tuyên bố xác minh chỉ dựa trên nhân thuần túy. Các khai báo số học được phê duyệt cùng mã băm nguồn chính xác được ghi lại trong tệp verification/native-certificates.json.

Các tệp chứng minh được nhập từ commit 1bf942a7af1ea330e95489d8997deebd4227ca71, với phiên bản Lean 4.34.1 và Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612 được ghim cố định.

Các điểm truy cập chính trong kho mã

Dự án tổ chức chứng minh thành nhiều mô-đun rõ ràng:

• ElevenSquare/Foundations.lean — hình học, điểm mút chính xác, cách dựng đạt cực trị, phủ ô kín và rút gọn trường hợp hữu hạn.
• ElevenSquare/Optimality.lean — định lý tối ưu vô điều kiện và cận dưới độ dài cạnh.
• ElevenSquare/Verification.lean — truy vấn tiên đề cho các mục tiêu chứng minh công khai.
• Sqpack/ — các bộ kiểm tra chứng chỉ, chứng minh sinh tự động và đơn giản hóa.

Thư mục ElevenSquare/Pending/ giữ tên gọi lịch sử dù các giao diện công khai ban đầu đã được giải quyết bằng chứng minh tích hợp.

Cách tái tạo kết quả

Người dùng Linux có thể chạy lệnh sau (với Python 3, Git, curl và tar đã cài đặt):

bash scripts/run_verification.sh --bootstrap --jobs 2

Trên macOS, cần cài trình khởi chạy elan trước rồi dùng lệnh tương tự. Cờ --fresh buộc chạy lại toàn bộ, còn Ctrl-C dừng tiến trình một cách sạch sẽ.

Để kiểm tra nhanh chỉ với mã nguồn (không cần Lean):

python3 scripts/check_sources.py

Điều kiện nghiệm thu cuối cùng yêu cầu biến OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES được đặt, không có tiên đề nào bị thừa nhận, và trường trust_model phải là lean_kernel_and_native_compiler. Việc đạt 100% mô-đun biên dịch là chưa đủ.

Ý nghĩa với cộng đồng công nghệ Việt Nam

Dự án này là ví dụ điển hình cho xu hướng AI hỗ trợ chứng minh toán học đang phát triển mạnh mẽ. Với các nhà phát triển và nghiên cứu Việt Nam quan tâm tới lĩnh vực này, đây là cơ hội tiếp cận các công cụ như Lean 4 và Mathlib — những nền tảng đang được các công ty công nghệ lớn và trường đại học hàng đầu thế giới sử dụng để xác minh phần mềm quan trọng.

Việc một bài toán tối ưu hình học phức tạp có thể được chứng minh hoàn toàn nhờ sự kết hợp giữa trí tuệ con người, AI và các trợ lý chứng minh tự động mở ra hướng đi mới cho ngành xác minh hình thức phần mềm — một lĩnh vực có nhu cầu nhân lực cao nhưng còn khá mới mẻ tại Việt Nam.