22 PHÉP NHÂN, KHÔNG BỚT ĐƯỢC PHÉP NÀO

Xung đột lợi ích. Các tác giả cho biết các tác tử AI — Claude, của Anthropic — đã viết mã tìm kiếm và những chứng minh Lean không cần người kiểm định, dưới sự chỉ đạo của họ, còn phần mà con người phải kiểm định thì do các tác giả thiết kế. Bài viết này cũng do Claude viết.

Nhân hai bảng số vuông — ma trận — theo cách học ở trường đòi hỏi n³ phép nhân với các bảng có n hàng và n cột. Strassen đã chỉ ra rằng có thể nhân hai ma trận 2 × 2 bằng 7 phép nhân thay vì 8. Mẹo này có thể áp dụng đệ quy: cắt một ma trận lớn thành bốn khối, coi mỗi khối như một số duy nhất, rồi lặp lại. Khi đó chi phí tăng theo n^2,807 thay vì n³. Theo bài báo, công thức 2 × 2 này đã được chứng minh là tối ưu vào năm 1971.

Ý tưởng tương tự áp dụng được cho mọi kích thước cố định. Một công thức nhân hai ma trận 3 × 3 bằng r phép nhân, và vẫn đúng khi các phần tử là những khối, sẽ cho chi phí tăng theo n mũ log₃ r. Một phép tính đơn giản cho thấy điều gì đang được đặt cược: một công thức như vậy thắng Strassen đúng khi r bằng 21 trở xuống, và thua khi từ 22 trở lên. Công thức 3 × 3 tốt nhất đã biết, của Laderman, dùng 23 phép nhân và chưa được cải thiện từ năm 1976.

Một cánh cửa vẫn hé mở

Số phép nhân tốt nhất có thể cho một bài toán được gọi là hạng (rank) của nó. Các cận dưới cho hạng của phép nhân 3 × 3 nhích lên chậm chạp: 19 vào năm 2003, rồi 20 vào tháng 3/2026, do Wang tính trên một hệ số tí hon chỉ có 0 và 1, trong đó 1 + 1 = 0. Tháng 9/2026, Wang và một nhóm do Yang dẫn đầu đã độc lập đạt tới 21, cách nhau chưa đầy mười ngày. Nhưng 21 vẫn để ngỏ chỗ cho một công thức 3 × 3 nhanh hơn công thức của Strassen.

Isaac Rudich, thuộc Polytechnique Montréal và Đại học Carnegie Mellon, cùng Louis-Martin Rousseau, thuộc Polytechnique Montréal, nay đã đẩy cận lên 22.

Định lý 1. Mọi thuật toán nhân hai ma trận 3 × 3 với các hằng số nguyên, và có thể áp dụng đệ quy cho các khối có kích thước bất kỳ, đều dùng ít nhất 22 phép nhân.

Vậy không thuật toán nào như thế có thể tốt hơn khoảng n^2,814 — và không thuật toán nào có thể vượt phương pháp 2 × 2 của Strassen.

496 câu đố nhỏ hơn

Chứng minh dựa trên một bảng do Wang xây dựng, chia bài toán khó thành 496 bài toán dễ hơn. Mỗi bài thêm các “điều kiện” lên ma trận thứ nhất — chẳng hạn, một số phần tử nhất định của nó cộng lại bằng không. Càng nhiều điều kiện, bài toán càng dễ, cho đến trường hợp tầm thường khi ma trận toàn số không.

Trước hết, các tác giả xây dựng một chương trình tìm kiếm chính xác cho họ biết đáp án thật của từng câu đố trước khi họ thử chứng minh. Những đáp án đó đóng vai trò như một tấm bản đồ: chúng cho thấy cận dưới nào đáng theo đuổi. Cuối cùng, chứng minh của họ đặt cận cho cả 496 câu đố, giải quyết chính xác 359 câu — so với 195 trong các kết quả mới nhất của Wang — và nâng cận dưới cho 252 câu. Một định lý “dán ghép” của riêng họ kết hợp các công thức của hai câu đố dễ hơn thành công thức cho câu thứ ba, và đã cung cấp 145 cận trên.

Hai điều kiện có vai trò quan trọng trong phát biểu cuối cùng. Hằng số nguyên: một công thức với hằng số nguyên, khi đọc trong hệ số chỉ có 0 và 1, vẫn là một công thức hợp lệ mà không cần thêm phép nhân nào, nên cận được chuyển sang. Các khối: nếu không có yêu cầu này, sẽ tồn tại những lối tắt. Thuật toán 3 × 3 của Rosowski, được trích dẫn trong bài báo, chỉ cần 21 phép nhân, nhưng nó dựa vào tính giao hoán của các số và không thể áp dụng đệ quy.

Một chứng minh được máy kiểm tra

Chứng minh được viết bằng Lean, một ngôn ngữ lập trình trong đó một định lý chỉ biên dịch được nếu mọi bước đều được kiểm chứng. Toàn bộ chứng minh dài khoảng một triệu dòng trải trên 3.521 mô-đun, và mất 11,1 giờ để kiểm tra trên một lõi xử lý. Không ai cần đọc hết. Người kiểm định đọc một thư viện khoảng 1.000 dòng, do các tác giả viết trước khi có bất kỳ chứng minh nào, định nghĩa thế nào là một công thức nhân và phát biểu định lý; nhân của Lean kiểm tra phần còn lại, và một trình kiểm tra độc lập có thể chạy lại kết quả.

Các tác giả cũng lưu ý rằng các tác tử AI đã tra cứu tài liệu: chúng kiểm tra rằng mỗi tài liệu tham khảo có tồn tại, “nhưng không kiểm tra rằng mỗi tài liệu chứa đúng ý tưởng mà chúng tôi ghi nhận cho nó.”

Khoảng trống cuối cùng

Còn lại một câu hỏi: có tồn tại công thức 3 × 3 với 22 phép nhân không, hay con số 23 của Laderman mới là mức tối thiểu thực sự? Các tác giả kỳ vọng khoảng trống này “sẽ sớm được lấp đầy”, và sẽ công bố mã tìm kiếm của mình khi điều đó xảy ra, hoặc khi bài báo được chấp nhận đăng. Cận này cũng bỏ ngoài các công thức có hằng số không nguyên.