Hệ Thống AI Của Axiom Math Xác Minh Một Định Lý Khó Về Số Nguyên Tố

Động thái này là lần đầu tiên nhóm tại Axiom Math tự động xác minh chứng minh của định lý 246 bằng hệ AxiomProver. Việc xác minh là dạng formal verification, tức máy tính kiểm tra phiên bản chứng minh đọc được bằng máy.

Bài viết lưu ý formal verification không phải là bảo đảm tuyệt đối, và có vụ việc trước đây cho thấy lỗi trong phương pháp có thể khiến hệ chấp nhận một chứng minh sai do AI tạo ra. Dù vậy, phương pháp tính toán này được coi là gần với một "con dấu thẩm định" nhất có thể.

Axiom Math trước đó đã dùng hệ đa-agent để biến các mệnh đề toán học thành chứng minh máy có thể kiểm tra, và đã giải một số bài toán chưa được giải và xác minh nhiều chứng minh trong năm nay. Theo nhóm, phần làm việc với định lý 246 nhằm xây dựng các thành phần có thể tái sử dụng cho những nhiệm vụ formalization và nghiên cứu toán học khác.

Nhóm đã dùng AxiomProver để tạo thư viện về các kết quả liên quan đến các khoảng cách giữa số nguyên tố, và định lý 246 là kết quả chủ lực trong thư viện đó. Một người tham gia, Sidharth Hariharan, cho biết nỗ lực lần này mang tính tổng quát và hữu ích hơn so với các nỗ lực một lần trước đây.