Axiom, công ty chuyên về AI cho toán học, thông báo cụm tác tử AxiomProver của họ đã hoàn tất hình thức hóa định lý phân loại nhóm đơn hữu hạn (CFSG) trong Lean chỉ sau 24 ngày, và gọi đây là bản chứng minh được máy tính kiểm tra đầy đủ đầu tiên của định lý này. Mã nguồn đã được mở trên GitHub theo giấy phép Apache-2.0. Kho mã tuyên bố phiên bản cuối không còn chỗ giữ chỗ sorry, không dùng native_decide, và chỉ dựa vào ba tiên đề chuẩn: tính ngoại diên của mệnh đề, tiên đề chọn cổ điển và tính đúng đắn của thương.
Phân loại nhóm đơn hữu hạn thường được gọi là “bảng tuần hoàn của đối xứng”. Định lý cho biết mọi nhóm đơn hữu hạn hoặc thuộc một trong 18 họ vô hạn, hoặc là một trong 26 nhóm rời rạc (sporadic). Chứng minh gốc nằm rải rác trong hơn 500 bài báo, dài khoảng 15.000 trang, do chừng 100 nhà toán học viết trong giai đoạn từ khoảng năm 1955 đến 2004. Phần cuối cùng, phần quasithin của Aschbacher và Smith, riêng một bài đã dài 1221 trang.
24 ngày đã diễn ra như thế nào
Theo quá trình Axiom công bố, dự án lập nhóm cộng tác trên Slack vào ngày 1 tháng 10, và lứa tác tử đầu tiên hoạt động từ ngày 2 tháng 10. Toàn bộ chứng minh được chia thành 108 cột mốc và khoảng 380 tác vụ nhỏ; các tác tử nhận việc qua issue trên GitHub và báo cáo tiến độ trên Slack. Tác tử chủ đạo phụ trách chia bài toán và rà soát các mệnh đề, những tác tử còn lại tra cứu kết quả có sẵn hoặc viết chứng minh Lean, và khi thiếu tiền đề thì giao việc xuống tiếp.
Quá trình không hề suôn sẻ. Một lô mã ban đầu bị xóa sạch vì sai sót do giả định ngầm, buộc nhóm phải lập kế hoạch lại. Về sau tốc độ biên dịch trở thành điểm nghẽn: các kỹ sư dùng bộ nhớ đệm, kiểm tra song song và đưa các phép tính hữu hạn ra ngoài dưới dạng chứng chỉ có thể kiểm chứng, nhờ đó rút thời gian build đầy đủ xuống dưới 24 giờ. Ngày 10 tháng 10, dự án đã công bố riêng việc chứng minh nhóm Monster là nhóm đơn.
Về ngữ liệu, Axiom cho biết họ đã đọc tổng cộng 715 bài báo và sách, đồng thời tái sử dụng khoảng 1,2 triệu dòng mã của dự án Qiuzhen-CFSG trước đó, cùng các thư viện hình thức hóa sẵn có như Mathlib và Tau Ceti.
Những sai sót được phát hiện nhân tiện
Trong quá trình hình thức hóa, nhóm đã ghi nhận 34 chỗ lệch toán học khá rõ. Chỗ được chú ý nhất nằm trên hướng chứng minh qua “định lý nhóm không cân bằng” (UGT): một khẳng định về bao đóng trong hồi ký năm 1986 của Walter có phản ví dụ, vì xuất phát từ PSL₂(49) sẽ suy ra PSL₂(7), mà nhóm này lại đúng là nhóm bị họ đó loại trừ. Một bổ đề của Aschbacher–Smith cũng bị tìm ra phản ví dụ SL₂(5); khi đẳng thức được đổi thành bất đẳng thức, lập luận phía sau phải được mở rộng theo.
Axiom đã công bố riêng một bài báo dài 35 trang về việc này, đề xuất lập luận thay thế và vá lại hướng chứng minh này với sự tham gia của các cố vấn như Lyons và Solomon. Công ty nhiều lần nhấn mạnh rằng các phản ví dụ này không bác bỏ chính UGT, càng không làm lung lay định lý phân loại.
“the classification remains the achievement of the mathematicians who discovered the groups”
(Phân loại vẫn là thành tựu của những nhà toán học đã khám phá ra các nhóm này.)
So với các lần kiểm chứng bằng máy trước đây
Xét theo chiều ngang, thứ hay được đem ra so sánh nhất là việc nhóm của Gonthier hoàn tất kiểm chứng định lý bậc lẻ trong Coq vào năm 2012. Định lý đó bắt nguồn từ bài báo dài 255 trang của Feit và Thompson năm 1963; dự án kéo dài khoảng sáu năm, và là một viên đá tảng trong chứng minh phân loại. Lần này Axiom bao phủ cả tòa nhà, và thời gian tính bằng ngày.
Hai bên không thể so tốc độ một cách trực tiếp. Dự án bậc lẻ năm đó gần như dựng thư viện từ đầu, còn Axiom đứng trên vai Mathlib và 1,2 triệu dòng mã CFSG đã có; số tác tử chỉ được nêu là “vài chục”, còn sức tính toán, phần cứng và tổng chi phí phía sau đều chưa được công bố, số giờ công cũng không được tiết lộ. 24 ngày là chu kỳ của chính dự án hình thức hóa, chưa tính đến hàng chục năm lao động của con người mà nó dựa vào.
Một vài điểm cần dè dặt cũng được ghi rõ. Siêu dữ liệu dự án đánh dấu phần rà soát là “tự đánh giá”, và hiện chưa có bên thứ ba nào tái lập bản build đầy đủ từ một môi trường sạch. Việc máy kiểm tra chỉ đảm bảo suy diễn đúng bắt đầu từ các giả thiết đã viết ra; các định nghĩa trong phát biểu phân loại có trung thành với định lý gốc hay không vẫn cần các nhà lý thuyết nhóm đối chiếu từng điều. Bài báo về UGT được đăng trên nền tảng preprint không qua bình duyệt đồng cấp, còn bảng đính chính, theo Axiom, sẽ được đặt trên trang dự án.
Với những người làm hình thức hóa, bước tiếp theo cần theo dõi hai điều: cộng đồng có tự chạy thông được 43,1 triệu dòng này hay không, và trong 34 chỗ lệch, có bao nhiêu chỗ được chính các tác giả gốc xác nhận.
Nguồn tham khảo: thông báo dự án và kho GitHub của Axiom, Unite.AI, CocoLoop, Kingy AI; số dòng mã Lean, số khai báo, số cột mốc và số chỗ lệch lấy theo số liệu do Axiom công bố, thời gian kiểm chứng định lý bậc lẻ theo tài liệu của Microsoft Research.