Axiom Math công bố bản chứng minh Lean dài 43,1 triệu dòng về phân loại nhóm

Các mô hình và nền tảng AI Axiom Math công bố chứng minh phân loại nhóm dài 43,1 triệu dòng bằng ngôn ngữ Lean Đăng ngày Ngày 27/10/2026 Tác giả Jonas Reeve, Tác tử nghiên cứu AI về AI nhận thức và AGI Thêm Unite.AI vào danh sách nguồn tin ưu tiên trên Google Ngày 27/10/2026, Axiom Math cho biết tổ chức này đang công bố công trình được coi là chứng minh hoàn chỉnh đầu tiên được máy tính kiểm chứng đối với Định lý Phân loại các nhóm đơn hữu hạn (CFSG). Công trình được hoàn thành trong 24 ngày bởi các kỹ sư và nhà toán học thông qua việc điều phối các nhóm gồm hàng chục tác tử AI (AI agent), tạo ra khoảng 43,1 triệu dòng mã trong hệ thống hỗ trợ chứng minh Lean. Trong thông cáo của mình, công ty nêu rõ: “Hôm nay, chúng tôi công bố chứng minh hoàn chỉnh đầu tiên được máy tính kiểm chứng đối với Định lý Phân loại các nhóm đơn hữu hạn (CFSG)”. Định lý phân loại này xác định các cấu tử cơ bản của các nhóm hữu hạn. Chứng minh nguyên bản kéo dài khoảng 15.000 trang trong hơn 500 bài báo của khoảng 100 nhà toán học; quy mô đồ sộ này khiến định lý có biệt danh là “định lý khổng lồ”. Nội dung Axiom công bố CFSG xác định rằng mọi nhóm đơn hữu hạn đều là nhóm cyclic cấp nguyên tố, nhóm thay phiên trên ít nhất năm ký hiệu, một trong 16 họ vô hạn của các nhóm kiểu Lie được xây dựng trên các trường hữu hạn, hoặc một trong 26 nhóm rải rác riêng biệt; thông báo cũng lưu ý một số tác giả coi nhóm Tits là nhóm thứ 27. Nhóm rải rác lớn nhất, nhóm Monster, được Robert Griess xây dựng vào năm 1980 bằng cách sử dụng một đại số 196.884 chiều. Nỗ lực chứng minh của các nhà khoa học đã kéo dài qua nhiều thập kỷ. Năm 1963, Walter Feit và John Thompson đã chứng minh rằng mọi nhóm đơn hữu hạn không giao hoán đều có cấp chẵn trong một bài báo dài 255 trang, chiếm trọn một số của tạp chí Pacific Journal of Mathematics. Daniel Gorenstein đã vạch ra chương trình 16 bước để hoàn thành việc phân loại vào năm 1972 và tuyên bố hoàn thành vào năm 1983. Tuy nhiên, trường hợp quasithin vẫn dựa trên một bản thảo chưa hoàn tất của Geoffrey Mason, cho đến khi Michael Aschbacher và Stephen Smith công bố công trình nghiên cứu dài 1.221 trang vào năm 2004, khép lại giai đoạn được gọi là chứng minh thế hệ thứ nhất. Một chứng minh thế hệ thứ hai có tính hệ thống hơn do Gorenstein và Richard Lyons khởi xướng, sau đó có sự tham gia của Ronald Solomon và Inna Capdeboscq, hiện vẫn chưa hoàn thành; do đó, Axiom đã tiến hành hình thức hóa chứng minh thế hệ thứ nhất. Trang thông tin của dự án giới thiệu quá trình hình thức hóa được thực hiện theo chứng minh thế hệ thứ nhất, với mọi bước logic đều được nhân của Lean kiểm tra; đồng thời liệt kê khối lượng dữ liệu gồm 43,1 triệu dòng mã Lean, 2,05 triệu khai báo, cùng 715 bài báo và sách. Axiom cho biết sơ đồ chứng minh của họ dựa trên các tài liệu thế hệ thứ hai, và quá trình hình thức hóa đã tích hợp khoảng 1,2 triệu dòng mã từ dự án Qiuzhen-CFSG trước đó, đồng thời phát triển dựa trên Mathlib với sự đóng góp của hàng trăm cộng tác viên. Dự án ghi nhận Dean Cureton, Vasily Ilin, Bhavik Mehta và Niels Voss là các cộng tác viên nòng cốt, cùng Letong Hong giữ vai trò chủ nhiệm đề tài. Kho lưu trữ công khai trên GitHub mô tả kết quả này là một chứng minh hoàn chỉnh trên Lean 4 không sử dụng lệnh giản lược "sorry" (sorry-free), cố định ở phiên bản 4.35.0-rc3, được xây dựng trên Mathlib cùng dự án TauCeti và chỉ sử dụng các tiên đề tiêu chuẩn gồm Classical.choice, propext, Quot.sound, không dùng native_decide. Phát biểu hình thức của định lý phân loại, được trích từ TauCeti, nêu rõ: “Mọi nhóm đơn hữu hạn đều đẳng cấu với một trong các nhóm được xây dựng tường minh trong danh sách phân loại”. Tệp README cho biết lệnh lake build kiểm tra toàn bộ quá trình phát triển; các điều chỉnh mở đối với công cụ Lake build cùng những tối ưu hóa mà nhóm dự kiến chuyển ngược về nhánh chính (upstream) đã giúp rút ngắn thời gian biên dịch xuống dưới 24 giờ; mã nguồn được phát hành theo giấy phép Apache-2.0. Nỗ lực phối hợp của mạng lưới AI trong 24 ngày Ngày 01/10/2026, Axiom đã mở một kênh Slack để điều phối dự án. Các kết quả nghiên cứu Lean có sẵn và một sơ đồ chứng minh nội bộ được tổng hợp từ các tài liệu đã công bố đã chia nhỏ nỗ lực này thành 108 mốc quan trọ ... và khoảng 380 nhiệm vụ nhỏ hơn; nhóm tác tử (swarm) đầu tiên bắt đầu vận hành vào ngày 2/10/2026, trong đó các tác tử nhận mốc công việc thông qua GitHub issues và báo cáo kết quả hoàn thành trên Slack. Các tác tử trưởng phân tích những lập luận phức tạp và thẩm định các mệnh đề, trong khi các tác tử khác tìm kiếm kết quả sẵn có hoặc viết chứng minh bằng Lean; đồng thời, một tác tử có thể ủy thác các điều kiện tiên quyết còn thiếu cho những tác tử khác có kết quả được đưa vào kho lưu trữ dùng chung. Tiến độ ban đầu đã bộc lộ những điểm yếu. Một số mốc công việc tưởng chừng khả thi lại ẩn chứa các điều kiện tiên quyết lớn mà các tác tử đã giả định thay vì chứng minh, và đội ngũ phát triển đã xóa hàng chục nghìn dòng lệnh được xây dựng trên các giả định đó trước khi tái khởi động với một kế hoạch chặt chẽ hơn; một mốc công việc ban đầu liên quan đến định lý hàm tử tín hiệu hóa (signalizer functor theorem), vốn có bản chứng minh dự kiến dựa trên các giả định cấu trúc vẫn cần được kiểm chứng. Thời gian biên dịch cũng trở thành điểm nghẽn khi các tác tử tạo ra các chứng minh nhanh hơn tốc độ Lean có thể kiểm tra lại. Axiom cho biết các kỹ sư của công ty đã phân phối kết quả biên dịch lưu trong bộ nhớ đệm (cache) cho các đơn vị xử lý (worker), thực hiện song song các bước kiểm tra độc lập và chuyển các phép tính hữu hạn tốn kém tài nguyên ra ngoài thành các chứng chỉ có thể kiểm tra riêng biệt; công ty cho biết những thay đổi này đã giúp tăng tốc độ xác thực lên nhiều bậc quy mô. Ngày 10/10/2026, một thông báo trên kênh trao đổi cho biết các tác tử đã chứng minh nhóm Monster là nhóm đơn, theo thuật lại của công ty; các tác tử cũng hình thức hóa sự tồn tại của nhóm Monster thông qua đại số Griess và một định lý đồng nhất các nhóm dạng Monster với nhóm Monster. Ngày 13/10/2026, chỉ có một mốc công việc được hoàn thành, và các kỹ sư đã tổ chức tái lập kế hoạch nhằm chia nhỏ các mốc công việc chưa hoàn thành thành các định lý nhỏ hơn, được phát biểu chính xác; mỗi phần phân tách đều được yêu cầu phải thể hiện rõ cách thức các cấu phần xác lập mốc công việc ban đầu thông qua một chứng minh ngắn bằng Lean. Những lỗ hổng được phát hiện trong chứng minh đã công bố Việc chuyển đổi chứng minh sang Lean đã bộc lộ những vấn đề trong các lập luận đã công bố, theo Axiom. Phần lớn là các lỗi nhỏ — lỗi ấn loát, sai sót trong bảng biểu hoặc bỏ sót giả thiết — nhưng công ty ghi nhận 34 sai lệch đáng chú ý so với các tài liệu đã công bố, trong đó sai lệch lớn nhất liên quan đến Định lý Nhóm không cân bằng (Unbalanced Group Theorem, hay UGT). Một ví dụ xuất phát từ các tập tài liệu về nhóm chuẩn mỏng (quasithin) của Aschbacher và Smith, trong đó một bổ đề khẳng định rằng hai