Microsoft Research và đồng tác giả chứng minh giả thuyết KLS 31 năm tuổi

Nhà nghiên cứu Microsoft Xinzhi Zhang và một đồng tác giả đã chứng minh giả thuyết Kannan-Lovász-Simonovits (KLS), một bài toán mở 31 năm tuổi trong hình học chiều cao, cho thấy cận đúng với một hằng số phổ quát độc lập với số chiều. Chứng minh này nảy sinh từ một quá trình tác tử do con người dẫn dắt, trong đó các tác tử AI đã khám phá hơn 100 hướng tiếp cận ứng viên trong khi các nhà nghiên cứu cắt tỉa và điều hướng tìm kiếm, và một nỗ lực không được dẫn dắt riêng rẽ với các mô hình hàng đầu trên ngân sách token tương đương đã không đạt được kết quả. Hai chứng minh khác xuất hiện cùng ngày, và một bản hình thức hóa bằng Lean 4 sau đó đã được công bố.