Axiom Math hình thức hóa thành công Stacks Project bằng AI

Trong bối cảnh các mô hình AI liên tục tung ra hàng trăm bản thảo toán học mỗi tháng mà không được kiểm chứng, startup Axiom Math đang đặt cược vào con đường ngược lại: kiểm chứng hình thức. Ngày thứ Tư vừa qua, công ty trị giá 1,6 tỷ USD thông báo đã chính thức xác minh hình thức (formal verification) toàn bộ Stacks Project — một trong những khối lượng toán học lớn nhất từng được con người viết ra.

Một "hố đen" của toán học đã được lấp

Stacks Project do nhà toán học Johan de Jong, đồng nghiệp của Peter Woit tại Đại học Columbia, khởi xướng năm 2005 như một tài liệu tham chiếu mã nguồn mở. Từ đó đến nay, cộng đồng toán học liên tục đóng góp, mở rộng từ đại số bậc đại học cho tới những ý tưởng tiên tiến nhất trong đại số, hình học và lý thuyết số.

Woit từng nhận xét Stacks Project "không có gì thực sự so sánh được", ví nó với "bộ sách Bourbaki nổi tiếng" — loạt sách đã xây dựng lại toán học từ nền tảng trong thế kỷ 20.

Đội ngũ AI agent của Axiom Math đã dịch khoảng 7.654 trang của thư viện này thành khoảng 16 triệu dòng mã được máy tính kiểm chứng. Về mặt lý thuyết, điều này lấp một khoảng trống lớn: theo Ashvin Swaminathan, thành viên nhóm kỹ thuật của Axiom, phần lớn toán học đã được hình thức hóa còn thiếu hụt nghiêm trọng, và "lỗ đen" đó bao trùm lên hình học đại số.

Kiểm chứng hình thức hoạt động thế nào?

Hình thức hóa toán học là cách đảm bảo cấu trúc nền tảng của một chứng minh là vững chắc. Các nhà toán học viết lại chứng minh dưới dạng mã trong ngôn ngữ lập trình Lean, rồi một chương trình gọi là proof assistant (trợ lý chứng minh) kiểm tra từng dòng mã. Nếu chứng minh vượt qua, họ có thể tin rằng nó đúng về mặt logic.

Ý tưởng tương tự, gọi là kiểm chứng hình thức (formal verification), đã được các kỹ sư dùng để xác nhận thiết kế chip, và các nhà nghiên cứu ở Pháp từng dùng để tìm lỗi trong phần mềm tính trợ cấp gia đình.

Với một thư viện như Stacks Project, kiểm tra từng định lý chỉ là một phần công việc. Các định lý và định nghĩa trong Stacks liên kết chặt chẽ với nhau, mỗi kết quả xây trên những kết quả trước đó, giống như một cây gia phả. Chính sự đan xen này khiến Axiom ban đầu không chắc dự án có khả thi.

"Những thứ lớn lao và những thứ mong manh trong cuộc sống vốn không đi cùng nhau," CEO Carina Hong nói với TechCrunch. "Bạn muốn các định lý nhất quán chứ không mâu thuẫn, muốn các định nghĩa không xung đột lẫn nhau."

Cách tiếp cận "vibe coding" có kiểm soát

Carina Hong, 25 tuổi, bỏ dở chương trình tiến sĩ toán tại Stanford và thành lập công ty vào tháng 3/2025. Cũng trong tháng 3, Axiom gọi được 200 triệu USD vòng Series A do Menlo Ventures dẫn dắt.

Để hoàn thành dự án, nhóm cho các agent một cấu trúc lỏng và để chúng chạy song song. "Với Stacks, chúng tôi áp đặt một hệ thống phân cấp… nhưng đó không phải hệ thống phân cấp hoàn chỉnh quy định từng agent làm gì," Swaminathan giải thích. "Các agent tự tìm nhiệm vụ và xác định những việc có thể làm song song."

Axiom cũng tự huấn luyện mô hình chuyên về toán — hướng đi mà Hong cho rằng hầu hết startup kiểm chứng khác không theo. Ban đầu, nhóm dựa vào một chuyên gia Lean nội bộ để dạy các agent "gu" của con người; về sau, Hong nói các agent đã tự hình thành gu riêng.

Nhà toán học Terence Tao của UCLA, người từng đoạt Huy chương Fields, đã tóm gọn logic cốt lõi: "Càng có nhiều chứng minh được hình thức hóa, bạn càng có thể tạo ra nhiều chứng minh được hình thức hóa hơn."

Không chỉ dành cho toán học

Toàn bộ kết quả đã kiểm chứng trở thành viên gạch nền, để các chứng minh tương lai dựa vào toán học đã được xác thực thay vì bắt đầu từ đầu. Nhưng đối tượng Axiom nhắm tới không chỉ là các nhà toán học.

Lập trình viên từ lâu đã chật vật trong việc đảm bảo mã không có lỗi và lỗ hổng bảo mật — vấn đề càng lớn khi AI agent viết ngày càng nhiều mã trên thế giới. Axiom đặt cược rằng phần mềm tương lai sẽ cần đứng trên nền tảng đã kiểm chứng, giống như Stacks hiện nay.

"Agent có thể đọc mã của chúng tôi, hiểu nó và xây hạ tầng mới lên trên. Bản hình thức hóa Lean của chúng tôi giờ là nền móng để agent xây tiếp," Swaminathan nói.

Hong tin rằng cách các agent của Axiom xây Stacks — chạy song song, tự chọn nhiệm vụ — sẽ là hình mẫu cho phần lớn công việc AI trong tương lai. Bà lập luận rằng agent cần một kho tri thức tái sử dụng, được xây dựng bài bản, để không sinh ra "rác".

"Nếu ngay từ đầu bạn thả vào những lựa chọn kỹ thuật tồi, thì rất khó để agent mở rộng biên giới về sau," Hong nói, đồng thời đưa ra lời thách thức: "Tôi công khai thách tất cả các công ty làm về lập trình cùng làm hình thức hóa ở quy mô này."

Góc nhìn

Với kỹ sư và doanh nghiệp Việt Nam, câu chuyện của Axiom Math gợi ra một hướng đi thực tế: khi AI agent viết ngày càng nhiều mã, giá trị chuyển dịch từ "viết nhanh" sang "đảm bảo đúng". Các nhóm phát triển phần mềm trong nước, đặc biệt ở lĩnh vực nhúng, tài chính hay hệ thống yêu cầu độ tin cậy cao, có thể bắt đầu tìm hiểu Lean và kỹ thuật kiểm chứng hình thức — hiện đã có tài liệu mở và cộng đồng trực tuyến.

Về dài hạn, nếu nền tảng toán học đã kiểm chứng trở thành chuẩn mực cho mã do AI sinh ra, các doanh nghiệp sớm xây dựng quy trình rà soát đầu ra của agent sẽ có lợi thế về chất lượng và bảo mật. Tuy nhiên, đây vẫn là một lĩnh vực non trẻ, đòi hỏi chuyên môn sâu và chưa có công cụ sẵn sàng cho mọi quy mô dự án.