Nhà nghiên cứu của Microsoft Research và cộng sự chứng minh giả thuyết KLS tồn tại 31 năm

Microsoft Research thông báo vào ngày 21 tháng 10 năm 2026 rằng Xinzhi Zhang, nhà nghiên cứu cấp cao thuộc nhóm Học máy và Tối ưu hóa của tổ chức này, cùng cộng sự Zhao Song đã chứng minh giả thuyết Kannan–Lovász–Simonovits, một bài toán tồn tại 31 năm trong hình học và xác suất nhiều chiều, bằng một quy trình nghiên cứu AI tác tử do con người định hướng.

Giả thuyết và cận mới

Chứng minh được trình bày trong bài báo dài 140 trang Một cận O(1) cho hằng số KLS, ghi tên Zhao Song và Xinzhi Zhang; bài báo được gửi lên arXiv lần đầu vào ngày 1 tháng 10 năm 2026 và sửa đổi vào ngày 4 tháng 10 năm 2026, với Zhang là tác giả gửi bài. Phần tóm tắt cho biết các tác giả chứng minh hằng số KLS ψ_n được chặn trên bởi một hằng số phổ quát C, qua đó giải quyết giả thuyết; họ cũng chứng minh một cận phổ quát cho hằng số Poincaré của mọi độ đo xác suất log-lõm đẳng hướng.

Về mặt hình thức, giả thuyết được đề xuất năm 1995 đặt câu hỏi liệu mọi độ đo xác suất log-lõm đẳng hướng trên không gian n chiều có hằng số Cheeger được chặn dưới bởi một hằng số dương phổ quát hay không. Diễn giải đơn giản hơn trong bài đăng của Microsoft Research là: với một lớp rộng các phân phối xác suất nhiều chiều, liệu phép cắt phẳng hoặc bằng siêu phẳng tốt nhất có luôn hiệu quả gần bằng phép cắt tốt nhất với hình dạng bất kỳ hay không, trong đó hiệu quả của hai phép cắt chỉ chênh lệch tối đa một hằng số phổ quát, bất kể số chiều là bao nhiêu. Vì hình học của các phép cắt này quyết định tốc độ bước đi ngẫu nhiên có thể khảo sát một phân phối, giả thuyết giữ vai trò trung tâm trong lý thuyết lấy mẫu nhiều chiều.

Trước công trình này, kết quả tốt nhất đã biết là bài báo dài 21 trang Hằng số KLS là O(log^{1/4} n) của Brayden Letwin, được gửi ngày 27 tháng 7 năm 2026. Công trình đó chứng minh ψ_n không lớn hơn một hằng số nhân với log^{1/4} n; bài đăng của Microsoft Research lưu ý rằng cận này vẫn tăng chậm khi số chiều tăng lên. Kết quả mới đạt được một cận cố định, không thay đổi theo số chiều.

Tầm quan trọng của giả thuyết đã được ghi nhận từ lâu trước khi nó được giải quyết. Bài đăng cho biết báo cáo thường niên 2017–18 của Mathematical Sciences Research Institute gọi KLS là một bài toán mở trung tâm trong hình học lồi nhiều chiều; Simons Institute mô tả đây là một trong những bài toán mở quan trọng nhất của hình học lồi; còn Ronen Eldan đã lưu ý đến những hệ quả rộng lớn của giả thuyết trong kỷ yếu Đại hội Toán học Quốc tế năm 2022.

Quy trình nghiên cứu bằng tác tử do con người định hướng

Theo bài đăng, các tác giả bắt đầu bằng việc tìm cách cải thiện kết quả tháng 7 năm 2026. Thông qua một quy trình có cấu trúc do con người định hướng, với sự tham gia của các tác tử AI, họ khảo sát hơn 100 hướng tiếp cận khả thi, nhiều hướng đòi hỏi những phép tính dài với tensor bậc cao, và đưa ra một tiêu chuẩn toán học mới làm nền tảng cho chứng minh cuối cùng.

Sau đó, các tác giả phát hiện có thể áp dụng tiêu chuẩn này theo cách đệ quy: đưa mỗi cận được cải thiện trở lại cùng một lập luận để tạo ra một cận chặt hơn nữa. Trong phiên bản bài báo ngày 1 tháng 10 năm 2026, cách làm này giảm mức phụ thuộc vào số chiều xuống còn logarit lặp, một đại lượng tăng cực kỳ chậm nhưng vẫn tăng theo số chiều, nên khi đó giả thuyết vẫn chưa được giải quyết. Bước cuối cùng là lặp lại toàn bộ quá trình tinh chỉnh đệ quy thay vì chỉ áp dụng một lần; theo bài đăng, ý tưởng này được gợi cảm hứng từ công trình trước đây của các tác giả về những thuật toán nhanh cho quy hoạch tuyến tính. Các tác giả chứng minh rằng những sai số nhỏ phát sinh ở mỗi giai đoạn giảm đủ nhanh để tổng của chúng vẫn được chặn bởi một hằng số phổ quát, không phụ thuộc vào số chiều, qua đó hoàn tất chứng minh trong phiên bản ngày 4 tháng 10 năm 2026.

Bài đăng cho biết phương pháp đệ quy, việc áp dụng phương pháp này nhiều lần và lập luận về sai số có tổng bị chặn là những đóng góp nguyên gốc của các nhà nghiên cứu. Các công cụ AI hỗ trợ khảo sát những hướng tiếp cận khả thi, thực hiện các phép suy diễn chi tiết, chuẩn bị bản thảo và kiểm tra chứng minh nội bộ; trong khi đó, các nhà nghiên cứu xác định hướng đi toán học, chọn những ý tưởng triển vọng, kết hợp chúng thành lập luận cuối cùng và kiểm chứng chứng minh. Bài đăng mô tả phương pháp này là tìm kiếm bằng tác tử kết hợp với quá trình sàng lọc lặp có sự hỗ trợ của con người: trong khi nhiều tác tử song song khảo sát các biến thể của một ý tưởng, nhà nghiên cứu xem xét kết quả trung gian, loại bỏ những hướng không triển vọng và chuyển kết quả triển vọng nhất sang vòng tiếp theo. Khoảng một trăm hướng nghiên cứu đã được khảo sát trước khi xuất hiện bước đột phá then chốt.

Trong một nhánh riêng của dự án, các tác giả đã nhiều lần thử giải cùng bài toán mà không có hướng dẫn, sử dụng một số mô hình AI hàng đầu với tổng ngân sách token xấp xỉ bằng quy trình chính; bài đăng cho biết nỗ lực này không đạt mục tiêu. Theo bài đăng, thành công cuối cùng phụ thuộc vào cả năng lực của các hệ thống AI lẫn khả năng phán đoán toán học của các nhà nghiên cứu. Bài đăng cảm ơn Song vì những đóng góp cho công trình, đồng thời cảm ơn Victor Reis và Ishai Menache vì những cuộc thảo luận trong suốt dự án.

Các chứng minh độc lập và kiểm chứng bằng máy

Ngày 4 tháng 10 năm 2026, cùng ngày bản chứng minh đầy đủ được đăng tải, Pierre Bizeul, Boaz Klartag và Joseph Lehec đã đăng một bản chứng minh dài 32 trang được phát triển song song, có tiêu đề *Trình bày một chứng minh cho giả thuyết Kannan-Lovász-Simonovits*. Tóm tắt của bài báo nêu rằng “bước then chốt trong chứng minh là tiêu chuẩn rất mới đây của Song và Zhang, liên quan đến các đạo hàm bậc cao của các giá trị trung bình nghiêng”; phần bình luận trên arXiv cũng lưu ý rằng bài báo có một đoạn mô tả việc sử dụng AI. Tóm tắt đặt KLS bên cạnh bài toán lát cắt của Bourgain và giả thuyết phương sai, xem đây là những động lực thúc đẩy các bước phát triển toán học trong hình học nhiều chiều suốt những thập kỷ gần đây.

Krishnakumar Balasubramanian và Shiva Kasiviswanathan đã đăng một chứng minh riêng có tiêu đề Một cận không phụ thuộc chiều cho hằng số Poincaré của các độ đo log-lõm đẳng hướng, lần đầu được gửi vào ngày 6 tháng 10 năm 2026 và sửa đổi vào ngày 8 tháng 10 năm 2026. Phần tóm tắt mô tả một chứng minh biến phân xác định với cận tường minh là 25 cho hằng số Poincaré của mọi độ đo xác suất log-lõm đẳng hướng.

Sau đó, một bản hình thức hóa bằng Lean 4 có tên KLS500 đã được xây dựng, hình thức hóa một hằng số Poincaré không phụ thuộc chiều, không lớn hơn 500, cho mọi phân phối xác suất log-lõm đẳng hướng. Theo kho lưu trữ, công trình này chủ yếu dựa trên phương pháp cumulant và phép treo của Bizeul, Klartag và Lehec, đồng thời tích hợp tiêu chuẩn độ nghiêng–phổ của Song và Zhang; quá trình kiểm chứng đã xây dựng lại 1.710 mô-đun toán học ở mức độ tin cậy bằng không của kernel. Lean cũng đã xác minh thành công phát biểu chính xác của giả thuyết KLS do OpenAI định nghĩa, sử dụng hằng số Poincaré phổ quát là 500. Dự án được cấp phép theo Apache 2.0.

Bài đăng của Microsoft Research mô tả các chứng minh độc lập là một trong những hình thức kiểm chứng mạnh mẽ nhất trong toán học, bởi chúng cho thấy một kết quả không chỉ dựa vào một chuỗi lập luận duy nhất. Bài đăng cho biết, khi giả thuyết đã được giải quyết, các kết quả trước đây dựa vào giả thuyết này như một giả định giờ đây có thể được phát biểu mà không cần điều kiện đó. Các tác giả đã rút gọn chứng minh và xác minh lập luận tinh gọn hơn bằng Lean; bài đăng cho biết họ dự định công bố cả hai sau khi hoàn tất khâu rà soát cuối cùng.