AI Agent Hyra của Tencent giải quyết bài toán 50 năm trong tổ hợp cộng tính

Tencent Hunyuan thông báo rằng agent AI nghiên cứu khoa học Hyra, phát triển trên mô hình Hy3, đã giải quyết thành công một bài toán mở kéo dài hơn nửa thế kỷ trong lĩnh vực tổ hợp cộng tính. Nhóm nghiên cứu đã công bố bản thảo bài báo khoa học cùng với chứng minh hình thức được xác thực bằng công cụ hỗ trợ chứng minh Lean. Thành tựu này làm nổi bật khả năng ngày càng tiến bộ của các agent AI trong việc hỗ trợ khám phá toán học phức tạp và xác thực hình thức. Bằng cách cung cấp chứng minh được xác thực qua Lean, nghiên cứu này giúp thu hẹp khoảng cách giữa các giả thuyết do AI tạo ra và các giải pháp chặt chẽ về mặt toán học được máy tính kiểm chứng. Bài toán liên quan đến việc phân tích mức độ mở rộng của một tập hợp số nguyên hữu hạn dưới phép cộng (tập tổng A+A) so với phép trừ (tập hiệu A-A). Mã nguồn cho cấu trúc tường minh và chứng minh hình thức bằng Lean đã được mở nguồn trên GitHub.