Axiom cho biết các tác nhân AI đã hình thức hóa Định lý phân loại nhóm đơn hữu hạn trong Lean

Axiom, một công ty AI về toán học, thông báo trên X rằng họ đã hoàn tất việc tự động hình thức hóa Định lý phân loại nhóm đơn hữu hạn bằng Lean, một kết quả mà công ty gọi là “bảng tuần hoàn của tính đối xứng”. Công ty mô tả chứng minh gốc dài khoảng 15.000 trang, do hơn 100 nhà toán học thuộc nhiều thế hệ thực hiện, và gọi đây là chứng minh toán học lớn nhất trong lịch sử được máy tính kiểm chứng.

Theo kho mã nguồn mở của Axiom, các nhóm tác nhân AI đã tạo khoảng 43,1 triệu dòng Lean trong 24 ngày, bao quát 715 bài báo và sách, đồng thời phát hiện 34 điểm khác biệt so với tài liệu đã xuất bản. Một bài đăng của tài khoản tin tức AI TestingCatalog cho biết thêm rằng các tác nhân chia việc như những nhóm phát triển phần mềm và viết mã nhanh hơn tốc độ Lean có thể kiểm tra.

Các số liệu này là theo chính Axiom; thông báo không đề cập đến việc có đánh giá độc lập nào về quá trình hình thức hóa. Tính đến ngày 28 tháng 10, bài đăng nhận được khoảng 6.200 lượt thích trên X.