Axiom Math phát hành chứng minh Lean dài 43,1 triệu dòng về phân loại nhóm

Ngày 27 tháng 10 năm 2026, Axiom Math cho biết họ đang phát hành thứ mà công ty gọi là chứng minh đầu tiên hoàn chỉnh, được máy tính kiểm tra, về Phân loại các nhóm đơn hữu hạn. Các kỹ sư và nhà toán học đã chỉ đạo hàng chục nhóm gồm nhiều tác nhân AI thực hiện chứng minh trong 24 ngày; các tác nhân viết khoảng 43,1 triệu dòng mã trong trợ lý chứng minh Lean.

“Hôm nay, chúng tôi phát hành chứng minh đầu tiên hoàn chỉnh, được máy tính kiểm tra, về Phân loại các nhóm đơn hữu hạn (CFSG),” công ty viết trong thông báo. Phân loại này xác định các khối cấu thành cơ bản của nhóm hữu hạn. Chứng minh ban đầu của nó trải dài khoảng 15.000 trang, trong hơn 500 bài báo do khoảng 100 nhà toán học viết, với quy mô lớn đến mức được đặt biệt danh là định lý khổng lồ.

Axiom phát hành những gì

CFSG xác lập rằng mọi nhóm đơn hữu hạn đều là nhóm cyclic có cấp nguyên tố, nhóm alternating trên ít nhất năm ký hiệu, thuộc một trong mười sáu họ vô hạn của các nhóm kiểu Lie được xây dựng trên trường hữu hạn, hoặc là một trong đúng 26 nhóm sporadic riêng lẻ. Thông báo lưu ý rằng một số tác giả tính nhóm Tits là nhóm thứ 27. Nhóm sporadic lớn nhất, Monster, được Robert Griess xây dựng vào năm 1980 bằng một đại số có số chiều 196.884.

Nỗ lực chứng minh của con người kéo dài hàng chục năm. 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 Pacific Journal of Mathematics. Năm 1972, Daniel Gorenstein đề ra chương trình gồm mười sáu bước để hoàn tất việc phân loại và tuyên bố công trình đã hoàn tất 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 chỉnh của Geoffrey Mason cho đến khi Michael Aschbacher và Stephen Smith công bố một công trình dài 1.221 trang vào năm 2004, khép lại phần được biết đến với tên gọi chứng minh thế hệ thứ nhất. Một chứng minh thế hệ thứ hai có hệ thống hơn, do Gorenstein và Richard Lyons khởi xướng, sau đó có thêm Ronald Solomon và Inna Capdeboscq tham gia, hiện vẫn chưa hoàn tất; vì vậy, Axiom đã hình thức hóa chứng minh thế hệ thứ nhất.

Trang dự án cho biết bản hình thức hóa này đi theo chứng minh thế hệ thứ nhất, với mọi bước lập luận đều được kernel của Lean kiểm tra; trang cũng liệt kê 43,1 triệu dòng Lean, 2,05 triệu khai báo và 715 bài báo, sách trong kho ngữ liệu. Axiom cho biết bản đồ chứng minh của họ dựa trên các tập sách thuộc chứng minh thế hệ thứ hai, còn bản 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 đó và được xây dựng dựa trên Mathlib, dự án mà công ty ghi nhận đóng góp của hàng trăm người. Dự án nêu tên Dean Cureton, Vasily Ilin, Bhavik Mehta và Niels Voss là những người đóng góp chủ chốt, còn Letong Hong là điều tra viên chính.

Kho lưu trữ GitHub công khai mô tả kết quả này là một chứng minh Lean4 không dùng sorry, được cố định ở phiên bản 4.35.0-rc3, xây dựng trên Mathlib và dự án TauCeti, đồng thời chỉ sử dụng các tiên đề chuẩn Classical.choice, propext và Quot.sound, không dùng native_decide. Phát biểu hình thức của định lý phân loại, lấy từ TauCeti, viết: “Mọi nhóm đơn hữu hạn đều đẳng cấu với một trong những nhóm được xây dựng tường minh trong danh sách phân loại.” README cho biết lake build kiểm tra toàn bộ công trình; những thay đổi đối với công cụ xây dựng Lake hiện vẫn đang mở và các tối ưu hóa mà nhóm dự định đưa vào dự án chính đã giúp rút thời gian xây dựng xuống dưới 24 giờ. Mã nguồn được cấp phép theo Apache-2.0.

Nỗ lực huy động một nhóm tác nhân trong 24 ngày

Ngày 1 tháng 10 năm 2026, Axiom mở một kênh Slack để điều phối dự án. Công việc Lean đã có từ trước cùng bản đồ chứng minh nội bộ được lập dựa trên các tài liệu đã xuất bản đã chia nỗ lực thành 108 mốc và khoảng 380 nhiệm vụ nhỏ hơn. Nhóm tác nhân đầu tiên bắt đầu hoạt động vào ngày 2 tháng 10 năm 2026; các tác nhân nhận thực hiện những mốc công việc thông qua các issue trên GitHub và báo cáo phần việc đã hoàn thành trên Slack. Các tác nhân chủ trì chia nhỏ những lập luận khó và rà soát các mệnh đề, trong khi những tác nhân khác tìm kiếm kết quả sẵn có hoặc viết chứng minh Lean. Một tác nhân cũng có thể giao cho các tác nhân khác tìm những điều kiện tiên quyết còn thiếu, rồi đưa kết quả của họ 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ó vẻ dễ xử lý lại ẩn chứa những điều kiện tiên quyết rất lớn mà các tác nhân mặc nhiên cho là đúng thay vì chứng minh; nhóm đã xóa hàng chục nghìn dòng mã được xây dựng dựa trên những giả định đó trước khi bắt đầu lại theo một kế hoạch vững chắc hơn. Một mốc ban đầu liên quan đến định lý hàm tử signalizer, trong đó chứng minh dự kiến dựa vào các giả định cấu trúc vẫn cần được biện minh. Thời gian xây dựng cũng trở thành nút thắt khi các tác nhân tạo ra chứng minh nhanh hơn tốc độ Lean có thể kiểm tra lại. Axiom cho biết các kỹ sư đã phân phối kết quả xây dựng được lưu trong bộ nhớ đệm giữa các máy xử lý, chạy song song các bước kiểm tra độc lập và chuyển những phép tính hữu hạn tốn kém thành các chứng chỉ riêng có thể kiểm tra độc lập. Theo công ty, những thay đổi này đã giúp tốc độ kiểm chứng tăng lên nhiều bậc độ lớn.

Ngày 10 tháng 10 năm 2026, một tin nhắn trên kênh thông báo rằng các tác nhân đã chứng minh Monster là nhóm đơn, theo lời kể của công ty. Các tác nhân cũng hình thức hóa sự tồn tại của Monster thông qua đại số Griess và một định lý xác định các nhóm kiểu Monster với Monster. Ngày 13 tháng 10 năm 2026, chỉ có một mốc được hoàn tất; các kỹ sư đã tổ chức một đợt lập kế hoạch lại, chia những mố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ép phân rã đều phải chỉ ra cách các phần hợp thành sẽ chứng minh được mốc ban đầu thông qua một chứng minh Lean ngắn.

Phát hiện khoảng trống trong chứng minh đã công bố

Axiom cho biết việc chuyển bản chứng minh sang Lean đã làm lộ ra những vấn đề trong các lập luận đã công bố. Phần lớn đều nhỏ — lỗi đánh máy, lỗi trong các bảng hoặc giả thiết bị bỏ sót — nhưng công ty ghi nhận 34 điểm sai khác đáng chú ý so với tài liệu đã công bố; điểm đáng kể nhất liên quan đến Định lý Nhóm Không Cân bằng, hay UGT.

Một ví dụ xuất hiện trong các tập sách về nhóm gần mỏng của Aschbacher và Smith, trong đó có một bổ đề khẳng định hai đại lượng bằng nhau. Các tác nhân phát hiện một phản ví dụ liên quan đến nhóm SL₂(5): một đại lượng có giá trị là 1, trong khi đẳng thức được khẳng định đòi hỏi giá trị đó phải là 2. Thay đẳng thức bằng bất đẳng thức đã sửa được bổ đề, nhưng các lập luận về sau dựa vào đẳng thức để loại trừ một số trường hợp, nên nhóm đã mở rộng một lập luận trước đó để bao quát những cấu hình ấy.

UGT giúp xác định một nhóm hoàn chỉnh từ thông tin về các nhóm con của nó: theo phần tóm tắt của bài báo đi kèm, với các giả thiết quy nạp của phép phân loại, nếu một nhóm con có cấp lẻ không tầm thường là nhóm con chuẩn tắc trong tâm hóa tử của một phép đối hợp, thì nhóm đơn bao chứa nó phải thuộc kiểu Lie trong đặc số lẻ hoặc là nhóm luân phiên có bậc thuộc một số giá trị nhất định. Axiom tiếp cận UGT thông qua chuyên khảo năm 1986 của John Walter; trong quá trình hình thức hóa lập luận đó, các tác nhân của công ty phát hiện những phản ví dụ cụ thể cho một khẳng định về tính đóng mà lập luận sử dụng: một phép toán được cho là giữ các nhóm đơn liên quan trong một họ nhất định lại có thể tạo ra một nhóm bị loại trừ rõ ràng khỏi họ đó.

Theo lời Axiom, bắt đầu từ PSL₂(49), mà phép đối hợp trường có tâm hóa tử là PGL₂(7), phép toán này cho ra thành phần đơn PSL₂(7). Nhóm này bị loại khỏi họ vì 7 là một số nguyên tố Mersenne. Axiom lưu ý rằng các phản ví dụ không bác bỏ chính UGT, thậm chí cũng không bác bỏ kết luận của Mệnh đề II.5.9(ii) của Walter.

Lập luận sửa chữa dựa trên lý thuyết năm 1976 của Solomon về các 2-thành phần cực đại; theo Axiom, lý thuyết này cung cấp những ý tưởng cốt lõi cho một lập luận thay thế do hệ thống AxiomProver tạo ra và hình thức hóa. Bước then chốt, được nêu trong bài báo là Định lý 2.3 (bảo toàn các đỉnh đơn), được Axiom mô tả là một kết quả mới trong lý thuyết nhóm do AxiomProver chứng minh. Kết hợp với các phép rút gọn của Gilman và Solomon cùng các định lý nhận dạng của Foote và Harris, kết quả này đưa ra dạng dành cho nhóm đơn của UGT cần thiết cho phép phân loại. Sau khi hoàn tất việc hình thức hóa, các nhà toán học của Axiom tìm ra một suy diễn ngắn hơn bằng các phương pháp thế hệ đầu, được ghi lại trong Nhận xét 9.5, đi đến cùng kết luận mà không cần Định lý 2.3.

Bài báo đó, The Unbalanced Group Theorem, do Colin Defant và Ken Ono đóng góp, được đăng trên máy chủ bản thảo Hexagon dưới dạng phiên bản 1 vào ngày 27 tháng 10 năm 2026 theo giấy phép CC BY 4.0; trang dự án ghi bài dài 35 trang. Axiom cho biết công ty đang làm việc với các nhà lý thuyết nhóm để tổng hợp những lỗi đính chính được tìm thấy trong tài liệu và sẽ công bố chúng trên trang đính chính của dự án. Lyons và Solomon, những người có công trình làm nền tảng cho phép phân loại, đã được tham vấn về việc sửa UGT; công ty cho biết sẽ tiếp tục tuyển chọn và xử lý các lỗi đính chính cùng một ban cố vấn có hai ông, bên cạnh cố vấn bên ngoài Dan Nakano. Axiom mô tả đóng góp của mình là giúp bản chứng minh có thể được kiểm tra bằng máy, ghi lại những trở ngại gặp phải và cung cấp các lập luận đã được hình thức hóa để giải quyết chúng, đồng thời khẳng định rằng thành tựu phân loại vẫn thuộc về các nhà toán học đã phát hiện ra những nhóm này và phát triển các lập luận.