Axiom Math Xác Minh Stacks Project Bằng AI Agent

Tháng trước, riêng OpenAI đã công bố 719 bản thảo nói rằng đã giải được một số bài toán khó nhất của lĩnh vực. Ngay cả các bước kiểm tra của máy cũng có thể trượt, nên nhiều người lo toán học có thể đi theo hướng nội dung rác do AI tạo.

Hôm thứ Tư, Axiom Math cho biết đã xác minh chính thức Stacks Project, một trong những bộ toán học lớn nhất do con người viết. Dự án này được Peter Woit của Columbia đánh giá rất cao, và ông so sánh nó với bộ sách Bourbaki, bộ đã xây dựng lại toán học từ nền tảng trong thế kỷ 20.

Johan de Jong của Columbia bắt đầu Stacks Project năm 2005 như một nguồn tham chiếu mã nguồn mở. Từ đó đến nay, các nhà toán học đã đóng góp liên tục, bổ sung kết quả từ đại số ở mức đại học đến các ý tưởng nâng cao trong đại số, hình học và lý thuyết số.

Đội ngũ AI agent của công ty đã chuyển thư viện khoảng 7.654 trang thành khoảng 16 triệu dòng code được máy kiểm tra. Cách làm là viết lại chứng minh trong ngôn ngữ Lean, rồi để một chương trình trợ giúp chứng minh kiểm tra từng dòng. Nếu qua được, các nhà toán học có thể tin rằng chứng minh đó hợp logic.

Cùng một ý tưởng này còn được kỹ sư dùng để xác nhận thiết kế chip hoạt động, và được các nhà nghiên cứu ở Pháp dùng để bắt lỗi trong phần mềm tính trợ cấp gia đình. Giám đốc điều hành Carina Hong nói những thứ lớn và những thứ mong manh thường không đi cùng nhau; bà cho biết Stacks là bộ kết quả toán học làm nền cho toán học, nên các định lý phải nhất quán và các định nghĩa không được mâu thuẫn. Hong 25 tuổi, từng bỏ chương trình tiến sĩ toán ở Stanford, lập công ty vào tháng 3/2025.

Tháng 3, Axiom huy động 200 triệu đô la trong vòng A do Menlo Ventures dẫn dắt. Để làm việc này, nhóm cho các agent một cấu trúc lỏng và để chúng chạy song song.