Phân loại nhóm đơn hữu hạn (CFSG) trong toán học hiện đại, có thể được coi là một trong những công trình chứng minh có quy mô lớn nhất.
Chứng minh này, được hoàn thành bởi hàng trăm nhà toán học qua nhiều thập kỷ, kết quả nằm rải rác trong hàng trăm bài báo và chuyên khảo, tổng độ dài gần hai mươi nghìn trang, khối lượng đã vượt xa khả năng xem xét lại toàn bộ của một cá nhân hay thậm chí một nhóm nghiên cứu.
Trong bối cảnh như vậy, việc đưa AI vào hỗ trợ kiểm tra chứng minh quy mô lớn trở thành một con đường mới cần phải thử.
Để thúc đẩy sự phát triển của AI cho Toán học, dưới sự đề xướng của ông Shing-Tung Yau, nhóm nghiên cứu đến từ sinh viên lớp Lãnh đạo của Học viện Chân Lý, Đại học Thanh Hoa, cùng với Trung tâm Khoa học Toán học Yau, Viện Nghiên cứu Công nghiệp Thông minh và Đại học Warwick, đã đề xuất FormaTheoria – quy trình làm việc hỗ trợ trí tuệ nhân tạo cho nghiên cứu toán học: để AI xuất phát từ tài liệu toán học gốc, tự động sắp xếp quan hệ phụ thuộc, tích hợp hệ thống tri thức và xây dựng chứng minh hình thức, cuối cùng giao cho trợ lý chứng minh Lean kiểm tra từng bước.
Tính đến tháng 8 năm 2026, FormaTheoria đã hoàn thành hình thức hóa bằng Lean cho bốn định lý then chốt, tạo ra hơn 994 nghìn dòng lý thuyết toán học được mã hóa có liên quan với nhau. Mặc dù còn một chặng đường dài để hoàn thành việc xác minh đầy đủ Phân loại nhóm đơn hữu hạn, nhưng thành quả này đã trở thành một cột mốc quan trọng hướng tới mục tiêu cuối cùng đó.
CFSG cung cấp hệ thống nền tảng cho nhiều thành tựu toán học quan trọng
“Phân loại nhóm đơn hữu hạn” nghe có vẻ rất trừu tượng. Nói một cách dễ hiểu, nó giống như một “danh sách các bộ phận cơ bản” về tính đối xứng hữu hạn: bất kỳ cấu trúc đối xứng hữu hạn phức tạp nào cũng có thể được phân tách thành nhiều lớp, cuối cùng thu được một loạt các đơn vị cơ bản không thể tiếp tục chia nhỏ; và vai trò của CFSG là nói cho các nhà toán học biết chính xác những đơn vị cơ bản này là những gì.
Thông thường, nghiên cứu toán học sẽ đầu tiên phân tách một vấn đề phức tạp xuống các đơn vị cơ bản này, sau đó xử lý từng loại dựa trên danh sách đầy đủ do CFSG cung cấp. Do đó, CFSG trở thành cơ sở hạ tầng mà các chứng minh khác có thể sử dụng bất cứ lúc nào. Nếu “cơ sở hạ tầng” này ẩn chứa lỗ hổng, thì rất nhiều kết quả tiếp theo được xây dựng dựa trên các kết luận liên quan của nó có thể bị ảnh hưởng.
Một số tổng quan chuyên môn cung cấp bằng chứng định lượng cho việc ứng dụng GFSG. Hiệp hội Toán học Hoa Kỳ đã xuất bản chuyên khảo của Stephen D. Smith “Applying the Classification of Finite Simple Groups: A User’s Guide” vào năm 2018, cuốn sách dày 231 trang, gồm 10 chương, tổng hợp các tình huống ứng dụng của GFSG. Hai chương cuối trong mục lục công khai liệt kê 14 chuyên đề ứng dụng được đánh số, bao gồm đồ thị truyền khoảng cách, giả thuyết Frobenius, thuật toán nhóm hoán vị, sự tăng trưởng nhóm con của nhóm hữu hạn sinh, mở rộng trường, phủ mặt Riemann, bài toán Waring trong lý thuyết nhóm, đồ thị mở rộng và nhóm xấp xỉ, v.v.
Giá trị ứng dụng của GFSG cũng được công nhận ở cấp độ cao nhất của cộng đồng toán học quốc tế. Đại hội các nhà toán học quốc tế 2014 đã mời Robert Guralnick, người đoạt giải Đại số Cole 2018 của Hội Toán học Hoa Kỳ, trình bày báo cáo chuyên đề có tiêu đề “Applications of the Classification of Finite Simple Groups”.
Những ứng dụng này bao gồm những thành tựu quan trọng có sức ảnh hưởng học thuật lớn. CFSG là mắt xích then chốt trong chuỗi chứng minh hoàn chỉnh cho bài toán Burnside hạn chế, Efim Zelmanov đã nhận được Huy chương Fields năm 1994 nhờ giải quyết vấn đề này. Chuyên khảo của Smith còn liệt kê bài toán Waring trên nhóm đơn hữu hạn và đồ thị mở rộng là hướng ứng dụng quan trọng của CFSG, các bài báo đại diện liên quan được công bố trên “Annals of Mathematics” (Bài toán Waring; đường kính nhóm đơn hữu hạn và ứng dụng). Những ví dụ này cho thấy, CFSG đã hỗ trợ một loạt công trình quan trọng giành được các giải thưởng học thuật hàng đầu và xuất hiện trên các tạp chí toán học đỉnh cao.
Từ ý nghĩa này mà xem, CFSG đã trở thành một hệ thống nền tảng được sử dụng lặp đi lặp lại. Khi các kết quả hạ nguồn ngày càng tích lũy nhiều, việc xác minh tính chính xác và khả năng kiểm tra lại của nó trở nên càng quan trọng. Việc kiểm tra máy móc có thể theo dõi, lặp lại đối với CFSG mang ý nghĩa vượt ra ngoài bản thân lý thuyết nhóm.
Tuy nhiên, khó khăn ở đây là, chứng minh của hệ thống nền tảng này đến từ các tài liệu thuộc các thời đại, tác giả và văn bản khác nhau, sử dụng các ký hiệu, định nghĩa và điều kiện mặc định thường không thống nhất, một trích dẫn thậm chí có thể dẫn đến cả một bộ tài liệu khác. Trong lịch sử, một lỗ hổng quan trọng trong chứng minh phân loại, phải đến hơn hai mươi năm sau mới được lấp đầy bởi một chuyên khảo hai tập, dày tới 1220 trang. FormaTheoria không chỉ cần kiểm tra từng bước suy luận, mà còn phải kiểm tra các định nghĩa, điều kiện và trích dẫn giữa hàng trăm tài liệu có thể kết nối hoàn chỉnh hay không, cuối cùng hình thành một chuỗi chứng minh không có điểm đứt gãy.
AI thúc đẩy công trình chứng minh siêu lớn như thế nào
Nhiều hệ thống AI toán học đối mặt với một bài toán đã được chuẩn bị sẵn, bao gồm đề bài, định nghĩa và công cụ đều sẵn sàng, AI chỉ chịu trách nhiệm tìm kiếm chứng minh. Nhưng FormaTheoria thì khác, nó cần đầu tiên xây dựng lại nền tảng toán học đằng sau đề bài từ một đống tài liệu rời rạc, rồi mới hoàn thành chứng minh. Công việc này chủ yếu đối mặt với bốn điểm khó:
Thứ nhất, hệ thống ban đầu không biết cần tham khảo bao nhiêu tài liệu.
Một trích dẫn có thể kéo theo một bài báo khác, bài báo đó lại dẫn đến nhiều công trình tiền đề hơn. Dự án ban đầu chỉ có 3 nguồn chính, trong quá trình chứng minh lại phát hiện thêm 12 nguồn; sau này bổ sung tài liệu chiếm 65.6% tổng số trang đã tra cứu. Cách xử lý của FormaTheoria là: một khi phát hiện thiếu một định lý tiền đề nào đó, sẽ tạm dừng chứng minh hiện tại, tìm kiếm và hình thức hóa mục phụ thuộc này, sau đó quay lại nhiệm vụ ban đầu để tiếp tục tiến lên. Kết quả đã được kiểm tra sẽ được lưu vào kho kiến thức thống nhất, để các chứng minh sau này lấy ra sử dụng nhiều lần.
Thứ hai, các tài liệu khác nhau rất khó ghép nối trực tiếp.
Các tác giả khác nhau sử dụng các định nghĩa, ký hiệu và điều kiện mặc định khác nhau. Hai định nghĩa trong toán học có thể hoàn toàn tương đương, nhưng một khi viết vào mã Lean, lại có thể không tương thích với nhau. FormaTheoria sẽ so sánh lặp đi lặp lại văn bản gốc và mã đã có, xây dựng các quan hệ chuyển đổi cần thiết. Đồng thời, hệ thống sẽ bảo vệ các phát biểu toán học đã được kiểm chứng, và kiểm tra xem mỗi lần sửa chữa có ảnh hưởng đến các chứng minh tiếp theo hay không. Bằng cách này, nhiều tác phẩm và bài báo độc lập với nhau mới có thể dần dần hòa nhập vào cùng một khung lý thuyết.
Thứ ba, mã thông qua kiểm tra vẫn có thể hiểu sai nguyên bản.
Lean chỉ chịu trách nhiệm kiểm tra logic chứng minh có tự nhất quán không, kết luận có được suy ra từ tiền đề không, nhưng không thể đánh giá kết luận này có trung thành với nguyên bản hay không. AI rất có thể bỏ sót một điều kiện nào đó, nhầm lẫn giữa “tất cả” và “tồn tại”, thậm chí sửa đổi sai kết luận. Vì vậy, FormaTheoria đặc biệt thiết lập một cửa kiểm tra độc lập: bộ phận dịch thuật viết ra phát biểu Lean trước, bộ phận kiểm tra sau đó đối chiếu với nguyên bản từng mục một. Trong 14 đoạn văn tài liệu được phân tích trong bài báo, 11 đoạn ở vòng dịch đầu tiên đều bị trả về sửa đổi. Cơ chế kiểm tra độc lập này, do đó trở thành “bảo hiểm” thứ hai bên cạnh việc kiểm tra máy móc.
Thứ tư, bản thân tài liệu gốc cũng có thể có vấn đề.
Trong tài liệu cũ có thể xuất hiện lỗi in ấn, thiếu điều kiện hoặc diễn đạt mơ hồ. FormaTheoria sẽ giữ lại trang gốc, đợi đến khi chứng minh sau này gặp mâu thuẫn, mới truy ngược lại để tra cứu. Nếu tài liệu có thể hỗ trợ sửa chữa, hệ thống sẽ bổ sung điều kiện hoặc thiết lập quan hệ tương thích; khi không đủ bằng chứng, hệ thống sẽ ghi lại vấn đề và giao cho chuyên gia toán học phán đoán.
Ngoài ra, công trình này còn yêu cầu AI duy trì nhịp độ trong một chu kỳ dài dằng dặc. Một lần đối thoại không thể chứa đủ toàn bộ nhiệm vụ. Vì vậy, FormaTheoria sử dụng một “bản đồ chứng minh” được cập nhật liên tục để quản lý tiến độ: các mục tiêu khó khăn hơn được chia nhỏ thành các bổ đề phụ trợ nhỏ hơn, kết quả thành công được tổng hợp từng lớp về định lý chính, các tuyến thất bại cũng được ghi lại, tránh việc hệ thống lặp đi lặp lại đi vào cùng một ngõ cụt.
Trên chiến lược song song, dự án cũng có thiết kế đặc biệt. Các nhiệm vụ độc lập với nhau có thể tiến hành đồng thời; nhiều nhiệm vụ nếu gặp cùng một kết quả tiền đề, hệ thống chỉ hoàn thành một lần và cho phép các nhiệm vụ khác sử dụng lại. Còn những nội dung toán học công cộng có thể ảnh hưởng đến toàn bộ thì được sửa đổi tuần tự từng cái một, tránh xung đột. Thí nghiệm đối chứng trong bài báo cho thấy, cách thức song song có nhận thức phụ thuộc này, đã đạt được tốc độ tăng tốc 4.2 lần trên các nhiệm vụ được thử nghiệm.
FormaTheoria từ đó hình thành một chuỗi công việc hoàn chỉnh: tìm kiếm tài liệu, bổ sung phụ thuộc, dịch nguyên bản, xây dựng chứng minh, kiểm tra máy móc, kiểm tra độc lập, phối hợp xung đột, và giao những vấn đề chưa chắc chắn cho chuyên gia toán học. Mỗi bước đều có trách nhiệm rõ ràng, có cơ sở để kiểm tra. Đây chính là thiết kế dựa trên những khó khăn thực tế xuất hiện trong các công trình chứng minh siêu lớn, nhằm trao quyền cho AI kết nối dần dần các tài liệu toán học rời rạc thành một hệ thống lý thuyết có thể kiểm tra, theo dõi và mở rộng bền vững.
△
Bảy tháng, bốn định lý then chốt, gần triệu dòng mã có thể kiểm tra
Ngày 22 tháng 1 năm 2026, FormaTheoria lần đầu tiên gửi mã, đến ngày 2 tháng 8 năm 2026, dự án đã thông suốt một chuỗi lý thuyết then chốt kéo dài đến định lý Bender–Suzuki, giữa chừng còn lần lượt hoàn thành chứng minh định lý Feit–Thompson về nhóm bậc lẻ, định lý Z* của Glauberman và định lý Brauer–Suzuki.
Bốn định lý này không hề tách biệt nhau, chúng tạo thành một tuyến quan trọng liên kết với nhau trong Phân loại nhóm đơn hữu hạn, chứng minh của định lý sau thường được xây dựng trên nền tảng toán học đồ sộ do định lý trước thiết lập.
Ảnh chụp nhanh dự án khi hoàn thành các chứng minh trên bao gồm:
- Hơn 994 nghìn dòng mã Lean ;
- Hơn 850 tệp mã ;
- Hệ thống đã tra cứu 15 cuốn sách và bài báo, tổng cộng 1037 trang , trong đó khoảng hai phần ba được phát hiện dần dần trong quá trình thúc đẩy chứng minh.
Tất nhiên, số dòng mã chỉ thể hiện một khía cạnh về quy mô công trình. Nếu lấy định lý Bender–Suzuki làm điểm kết thúc và truy ngược về trước, dự án đã hình thành một mạng lưới chứng minh chứa 30298 phát biểu toán học, 186187 quan hệ phụ thuộc , chuỗi phụ thuộc dài nhất đạt 458 lớp. Nếu tính cả nội dung liên quan trong thư viện cơ sở của Lean, mạng lưới này sẽ mở rộng đến 74922 phát biểu và hơn 1.44 triệu quan hệ phụ thuộc. Có thể nói, đằng sau gần triệu dòng mã là một mạng lưới chứng minh chằng chịt, liên kết chặt chẽ. Nghiên cứu này cho thấy, tác nhân thông minh AI đã có thể dưới sự hợp lực của việc kiểm tra máy móc và kiểm tra phân lớp, thúc đẩy liên tục các công trình toán học lớn, siêu dài hạn.
Quá trình vận hành thực tế của dự án cũng mang đặc tính siêu dài hạn. Lần thực thi tác nhân thông minh dài nhất được ghi lại trong bài báo kéo dài 9.17 ngày, trong thời gian đó hệ thống đã thực hiện 606 lần nén và sắp xếp thông tin tích lũy, đồng thời luôn giữ lại mục tiêu chứng minh hiện tại, kết quả đã hoàn thành, và các vấn đề vẫn còn tồn đọng. Những dữ liệu này cho thấy, quản lý dự án đang duy trì một mạng lưới chứng minh siêu dài hạn không ngừng tiến hóa, việc tạo ra đơn lẻ hoặc một lần đối thoại hoàn toàn không thể bao quát được quá trình phức tạp như vậy.
Trước đây, việc hình thức hóa toán học quy mô lớn chỉ có thể phụ thuộc rất nhiều vào sự đầu tư nhân công, thường cần nhiều nhà nghiên cứu hợp tác liên tục trong nhiều năm. Một tham chiếu lịch sử để so sánh: phiên bản hình thức hóa Rocq trước đây của định lý Feit–Thompson, được hoàn thành bởi khoảng 15 người mất sáu năm. Trong khi đó, FormaTheoria đã hoàn thành toàn bộ nội dung của dự án nhân công đó trong bảy tháng, và mở rộng hơn nữa đến công việc hình thức hóa các định lý then chốt khác. Bảy tháng đối với một nhiệm vụ tác nhân thông minh AI, vẫn là một chu kỳ vận hành cực kỳ dài, nhưng so với hình thức hóa thủ công truyền thống, sự can thiệp của AI đã rút ngắn đáng kể thang thời gian vận hành dự án.
△
Hình thức hóa khiến các vấn đề ẩn trong tài liệu lộ ra từng cái một
Tài liệu toán học thường hướng đến những nhà nghiên cứu quen thuộc với lĩnh vực đó. Vì vậy, tác giả thường bỏ qua các điều kiện đã xuất hiện trước đó, hoặc mặc định người đọc có thể nhận ra quan hệ tương đương giữa các định nghĩa khác nhau. Một số lỗi in ấn nhỏ hoặc lỗi ký hiệu, khi đọc thủ công thường bị bỏ qua hoặc sửa chữa một cách tự nhiên. Nhưng cách làm của FormaTheoria thì khác, khi nó dịch từng dòng tài liệu thành mã Lean, mỗi định nghĩa, mỗi điều kiện và mỗi bước suy luận đều phải được viết rõ ràng, không mơ hồ. Chính yêu cầu kiểm tra từng dòng nghiêm ngặt này đã khiến những vấn đề vốn ẩn giấu trong tài liệu gốc trở nên rõ ràng.
Bài báo ghi chép chi tiết nhiều loại vấn đề tài liệu mà dự án phát hiện, bao gồm các tài liệu khác nhau đưa ra định nghĩa không nhất quán cho cùng một khái niệm, phát biểu định lý bỏ sót điều kiện cần thiết, điều kiện chia hết viết sai vị trí, thậm chí chỉ số dưới trong chứng minh cũng có sai sót. Một phần trong số các vấn đề này có thể tự động sửa chữa dựa trên ngữ cảnh tài liệu; những vấn đề không đủ bằng chứng sẽ được giao cho nhà toán học tiếp tục đánh giá.
Một trường hợp điển hình đến từ hai tài liệu về định lý nhóm bậc lẻ. Cả hai tài liệu đều định nghĩa “nhóm con cực đại loại I”, nhưng khác biệt ở chỗ: một tài liệu yêu cầu một tính chất nào đó phải đúng với “mọi cấu trúc bù”; tài liệu kia chỉ yêu cầu “tồn tại một cấu trúc bù” thỏa mãn tính chất đó. Về hình thức, cái trước rõ ràng mạnh hơn cái sau, do đó hai bộ định nghĩa không thể kết nối trực tiếp. FormaTheoria trong quá trình hình thức hóa đã nhạy bén nhận ra sự khác biệt này, sau đó dựa vào định lý Schur–Zassenhaus, chứng minh hai định nghĩa ở đây thực tế tương đương, từ đó thành công xây dựng cầu nối liên kết hai tài liệu.
Một trường hợp khác đến từ một bổ đề của Peterfalvi. Trong phát biểu chính thức của bổ đề này đã bỏ sót điều kiện tiên quyết “cấp của một nhóm nào đó là số lẻ”, tuy nhiên chứng minh sau đó thực tế không thể thiếu điều kiện này. Mặc dù khi áp dụng bổ đề này ở phần sau, phần trước đã đảm bảo điều kiện này, toàn bộ lập luận không bị đứt đoạn, nhưng Lean sẽ không tự động bổ sung thông tin nền tảng này. FormaTheoria sau khi truy vết đường dẫn chứng minh và vị trí sử dụng của bổ đề đó, đã tự động thêm điều kiện bị bỏ sót vào phát biểu định lý, làm cho toàn bộ chuỗi hình thức hóa trở nên hoàn chỉnh và đáng tin cậy hơn.
△
Dự án còn phát hiện ra lỗi tài liệu trực tiếp hơn. Một định nghĩa viết đối tượng H lẽ ra phải xuất hiện thành M, và hai tài liệu tham khảo đều giữ nguyên lỗi sai đó. Một định lý của Huppert lại đưa thừa số d vào điều kiện chia hết sai; hệ thống tìm thấy phản ví dụ và dừng chứng minh, giao vấn đề cho nhà toán học kiểm tra. Con người đã xác nhận điều kiện chính xác. Một đoạn chứng minh của Higman còn viết số chỉ của một tập vectơ cơ sở thành từ u0 đến um, phạm vi đúng phải là đến um−1; lỗi chỉ số dưới này đã được hệ thống tự động nhận dạng và sửa chữa trong quá trình chứng minh.
Những trường hợp này phản ánh một giá trị quan trọng khác của việc kiểm tra máy móc đối với các công trình toán học lớn. FormaTheoria trong khi xây dựng chứng minh hình thức, cũng tiến hành kiểm tra chi tiết đối với tài liệu gốc: nó ghi lại vấn đề xuất hiện ở đâu, chứng minh tiếp theo cần điều kiện gì, cơ sở sửa đổi đến từ tài liệu nào, và việc sửa chữa có ảnh hưởng đến các kết quả khác hay không. Đối với CFSG được tạo thành từ hàng trăm tài liệu liên kết với nhau, cơ chế kiểm tra có thể theo dõi này có thể chuyển hóa những chi tiết trước đây phụ thuộc vào kinh nghiệm của người đọc để bổ sung, thành cơ sở toán học có thể kiểm tra rõ ràng.
Triển vọng tương lai
FormaTheoria hiện tại chưa hoàn thành việc hình thức hóa toàn bộ Phân loại nhóm đơn hữu hạn, vẫn còn một chặng đường dài để đến mục tiêu cuối cùng. Dự án đang được đẩy nhanh tiến độ, tiếp tục hướng tới việc hoàn thiện hình thức hóa một trong những công trình chứng minh có quy mô lớn nhất của toán học hiện đại. Kết quả hiện có cho thấy, AI đã có thể trong vòng vài tháng duy trì và mở rộng môi trường toán học quy mô lớn, vượt qua nhiều tài liệu để theo dõi các quan hệ phụ thuộc phức tạp, xây dựng các hệ thống lý thuyết liên kết với nhau, có khối lượng khách quan dưới sự kiểm tra nghiêm ngặt. Ranh giới khả năng của AI, từ đó cũng bắt đầu từ việc giải quyết các bài toán toán học riêng lẻ, dần dần mở rộng đến việc tham gia xây dựng tri thức toán học có hệ thống.
Công việc này còn sẽ hình thành một cơ sở hạ tầng toán học có thể mở rộng bền vững, có thể sử dụng lại. Tài liệu truyền thống chỉ có thể nói cho người đọc biết “chứng minh viết ở đâu”; mã hình thức hóa còn ghi lại “mỗi kết luận phụ thuộc vào cái gì”, “các nguồn khác nhau kết nối thế nào”, “những vấn đề nào đã được sửa chữa”, và tổ chức các định nghĩa, bổ đề, chứng minh đã được kiểm chứng thành các mô-đun tri thức mà nghiên cứu sau này có thể trực tiếp gọi sử dụng. Một khi trong tương lai thêm vào các công cụ giải thích, tìm kiếm và trực quan hóa, mạng lưới tri thức này hy vọng sẽ giúp các nhà nghiên cứu nhanh chóng hiểu được cấu trúc tổng thể của CFSG, sử dụng lại các thành quả đã có, thậm chí cung cấp hỗ trợ mạnh mẽ cho các nhà toán học con người khám phá các mối liên hệ mới và phát hiện định lý mới.
Nhóm dự án FormaTheoria hy vọng khám phá một mô hình hợp tác người-máy hướng tới thời đại AI: con người chịu trách nhiệm xác định các vấn đề đáng nghiên cứu và đưa ra phán đoán then chốt, AI đảm nhận tìm kiếm và suy luận quy mô lớn, hệ thống hình thức đảm bảo mỗi bước được chấp nhận đều có thể được kiểm tra lại. Khi một chứng minh trở nên lớn đến mức bất kỳ cá nhân nào cũng khó có thể kiểm tra lại từ đầu, cách thức kết hợp ba điều này có lẽ sẽ trở thành một con đường hoàn toàn mới để con người quản lý tri thức toán học siêu lớn.
Lưu ý: Trạng thái dự án và kết quả định lượng trong bài dựa trên ảnh chụp nhanh khi hoàn thành vào tháng 8 năm 2026 như mô tả trong bài báo.
Bài báo: https://arxiv.org/abs/2608.10894
Mã nguồn: https://github.com/Qiuzhen-CFSG/CFSG
Bài viết này đến từ tài khoản WeChat công chúng “量子位”, tác giả: Đội ngũ FormaTheoria
