Axiom Hình Thức Hoá Phân Loại Nhóm Đơn Hữu Hạn Bằng Lean: 43,1 Triệu Dòng Trong 24 Ngày

Ngày 27/10/2026 (trên blog ghi 26/10), công ty Axiom Math công bố họ đã dựng xong bản chứng minh Lean đầu tiên của Định lý phân loại nhóm đơn hữu hạn (CFSG), thứ thường được coi là chứng minh dài nhất lịch sử toán học, khoảng 15.000 trang do cỡ 100 nhà toán viết. Theo Axiom, đàn tác tử AxiomProver cùng kỹ sư và nhà toán làm trong 24 ngày, ra khoảng 43,1 triệu dòng Lean, 2,05 triệu khai báo, và trên đường đi phát hiện một lập luận đã đăng bị sai ở Định lý nhóm không cân bằng. Mã nguồn công khai, không còn "sorry", chỉ dùng ba tiên đề chuẩn. Nhưng hồ sơ của chính Axiom ghi trạng thái rà soát là "tự đánh giá", chưa ai công bố đã dựng lại toàn bộ, và con số lỗi trong văn liệu thay đổi từ 34 đến "hơn 2.000" tuỳ nguồn. Locaith đọc blog, kho mã, bản thảo và tệp số liệu của trang, rồi tách phần đã kiểm được khỏi phần vẫn là lời hãng.

Axiom công bố gì, và theo trình tự nào

Bài blog của Axiom (đề ngày 26/10/2026) nói họ đã "phát hành bản chứng minh được máy kiểm tra đầu tiên và hoàn chỉnh" của CFSG, bám theo chứng minh thế hệ thứ nhất. Chứng minh thế hệ thứ hai của Gorenstein, Lyons, Solomon và Capdeboscq chưa hoàn tất (ít nhất 12 tập, tới 2023 mới có 10), nên Axiom chọn thế hệ thứ nhất. Kho GitHub AxiomMath/CFSG được tạo lúc 13:19 UTC ngày 27/10 (theo API GitHub), bài đăng chính thức của Axiom trên X lúc 14:34 UTC cùng ngày. Trình tự theo blog:

Từ 2/10 (ngày đàn đầu tiên chạy) đến 26/10 là 24 ngày; blog tính "24 ngày" cho cả dự án nên Locaith coi đó là khoảng thời gian của riêng đợt hình thức hoá này, không phải công sức tổng cộng. Bài của kingy.ai cũng nhấn mạnh Axiom chưa công bố chi phí tính toán, phần cứng, danh sách đầy đủ mô hình hay số giờ người. Blog chỉ nói đàn gồm "hàng chục" tác tử và dùng "một tổ hợp mô hình thay đổi". Để so cỡ: Feit–Thompson (255 trang) được Gonthier và cộng sự hình thức hoá trong Coq năm 2012 sau sáu năm (theo blog); Locaith đã viết về dự án Claude 13 triệu dòng Lean cho Định lý lớn Fermat, nhưng đó là dịch chứng minh có sẵn của Wiles, không phải một chứng minh trải trên hàng trăm bài báo.

Cái gì do máy kiểm, cái gì vẫn là lời của Axiom

Phần máy kiểm là phần Lean làm được: README của kho ghi bản chứng minh dùng Lean 4 (v4.35.0-rc3) trên Mathlib và dự án TauCeti, "không có sorry", chỉ dùng ba tiên đề chuẩn Classical.choice, propext, Quot.sound, không dùng native_decide. Tệp formalization.yaml ghi sorry_count bằng 0 và hai kết quả chính, trong đó CFSGComparator.classification được kiểm bằng cấu hình comparator.json (tệp Challenge.lean chứa phát biểu với "sorry", tệp Solution.lean chứng minh nó từ CFSG.Certified.classification_finite_simple_groups). Locaith đã đọc các tệp này nhưng không chạy lại lake build hay comparator: kho nặng khoảng 6 GB (theo API GitHub), README nói cần thay đổi Lake chưa đưa vào bản chính để dựng dưới 24 giờ.

Phần vẫn là lời của Axiom hoặc cần người đọc kiểm:

• Phát biểu cuối cùng không do Axiom viết. Nó lấy nguyên từ dự án TauCeti: mọi nhóm hữu hạn đơn đều đẳng cấu với một nhóm trong danh sách (xyclic cấp nguyên tố, nhóm thay phiên, kiểu Lie, 26 nhóm rời rạc). Chính chú thích của TauCeti nói tệp này "chỉ là phát biểu", không khẳng định các nhóm trong danh sách là hữu hạn hay đơn; các nhóm kiểu Lie dùng tập nền tường minh mà việc đồng nhất với các lược đồ nhóm đơn liên đã chỉ định "được xử lý riêng"; các nhóm rời rạc được định nghĩa bằng biểu diễn hữu hạn mà không giả định định lý nhận dạng. Blog nói con người kiểm phát biểu và các định nghĩa nó dùng, còn Lean kiểm các suy diễn dẫn tới nó.
• Chiều ngược lại (các nhóm trong danh sách tồn tại và đơn). Blog nói đã chứng minh (ví dụ nhóm Quái vật đơn); tệp formalization.yaml liệt kê kết quả chính thứ hai CFSG.Milestones.cfsg_classification_native_and_realization. Locaith không mở tệp đó.
• Trạng thái rà soát. Tệp formalization.yaml ghi mục review: status "self-assessed", người rà soát "Axiom Math", phương pháp "autonomous", khung "AxiomProver", literature_dependencies rỗng. Bài của kingy.ai nói họ chưa dựng lại bản build lẫn chưa kiểm toán độc lập; Locaith cũng không tìm thấy bản dựng lại hay kiểm toán toán học từ bên ngoài tính đến 28/10 (không có nghĩa là chưa có).
• Không phải chứng minh đã đăng. Chính blog nói một hình thức hoá có thể đi đường khác với lịch sử (họ thay một bước của Walter bằng lập luận khác). Câu "chứng minh dài nhất lịch sử nay đã được máy kiểm" trên X đúng với nghĩa "một chứng minh thế hệ thứ nhất, có sửa", không phải "bản in 15.000 trang được kiểm từng chữ".

Locaith đọc lại số liệu của chính trang Axiom

Trang cfsg.axiommath.ai nạp số liệu từ tệp lean_meta.json (commit 3e39d100 của kho). Locaith tải tệp này ngày 28/10 và đối chiếu với những gì trang hiển thị:

• 43,1 triệu là "dòng vật lý". Cùng tệp có hai trường: physical_lines = 43.068.312 (số trang chủ hiển thị) và lines = 35.093.004, chênh khoảng 23%. Trang không định nghĩa chênh lệch này (Locaith không đoán nó là dòng trống hay chú thích). Trên 221.155 tệp, trung bình khoảng 195 dòng vật lý mỗi tệp.
• "2,05 triệu khai báo" là một tập con. Tệp ghi 2.216.163 khai báo trong tổng, và 2.053.885 (khoảng 92,7%) ở trường in_final, trường mà trang chủ lấy. Locaith đọc "in_final" là các khai báo nằm trong phần phụ thuộc của định lý cuối, nhưng trang không giải thích tên trường.
• Phần "danh sách" nhỏ, phần "vét cạn" lớn. Ba thư mục LieType, Sporadic và Monster cộng lại 1,46 triệu dòng (khoảng 4,2% trong 35,09 triệu). Local analysis một mình chiếm 14,02 triệu (40,0%), Quasithin 4,69 triệu, Rank three 3,55 triệu. Phần khó của CFSG nằm ở chỗ chứng minh danh sách đã đầy đủ, khớp với mô tả của blog.
• Mã mượn và dữ liệu chứng chỉ. Blog nói dùng lại khoảng 1,2 triệu dòng từ dự án Qiuzhen-CFSG; thư mục ThirdParty trong tệp số liệu có 1,27 triệu dòng. Hai thư mục chứng chỉ cộng 2,21 triệu dòng (6,3%) và là mô-đun Lean (CertifiedResults.lean nhập từng Certificates.CertificateN). Ngoài ra, trong phần cây thư mục mà API GitHub trả về (bị cắt ở 65.141 mục) có ít nhất khoảng 3 GB tệp không phải .lean (.bin, .items, .txt, .gz) nằm dưới thư mục CFSG/Certificates; README không giải thích vai trò của chúng và Locaith không mở. Blog chỉ nói các phép tính hữu hạn tốn kém được "đưa ra thành chứng chỉ có thể kiểm riêng".

Lỗi trong văn liệu: 34, "hàng trăm", hay "hơn 2.000"?

Ba nguồn đưa ra ba cỡ số khác nhau, và chúng không cùng đo một thứ:

Ví dụ cụ thể blog nêu từ các tập "quasithin" của Aschbacher và Smith: một bổ đề khẳng định hai đại lượng bằng nhau, nhưng với nhóm SL₂(5) một đại lượng bằng 1 trong khi đẳng thức đòi 2. Sửa thành bất đẳng thức thì một số lập luận sau đó từng dùng đẳng thức để loại trường hợp phải xét lại; nhóm Axiom mở rộng một lập luận trước đó để xử lý.

Định lý nhóm không cân bằng: lỗi nằm ở đâu và bản thảo là gì

Lỗi đáng kể nhất nằm ở chứng minh của John Walter (1986) cho Định lý nhóm không cân bằng (UGT). Tác tử tìm thấy phản ví dụ cho một khẳng định "đóng" trong chứng minh: một phép toán được cho là giữ các nhóm đơn trong một họ nhất định, nhưng có thể sinh ra nhóm bị loại khỏi họ. Phản ví dụ blog nêu: PSL₂(49), với phép đối hợp trường là một tự đẳng cấu của nó; tâm hoá của phép này là PGL₂(7), thành phần đơn là PSL₂(7), mà PSL₂(7) bị loại vì 7 là số nguyên tố Mersenne. Blog nhấn mạnh phản ví dụ không bác bỏ UGT lẫn kết luận Mệnh đề II.5.9(ii) của Walter; nó chỉ làm một bước suy diễn mất cơ sở. Axiom thay bằng lập luận dựa trên lý thuyết "2-thành phần cực đại" của Solomon (1976), do AxiomProver tạo ra và hình thức hoá, rồi nêu thành Định lý 2.3 ("bảo toàn đỉnh đơn"), được trình bày là kết quả mới của lý thuyết nhóm.

Có hai điều cần đọc kèm. Một: sau khi hình thức hoá xong, các nhà toán tại Axiom tìm ra một đường tắt ngắn hơn (Nhận xét 9.5 trong bản thảo) cho cùng kết luận UGT mà không cần Định lý 2.3; theo blog, bản thảo giữ cả hai. Locaith chỉ đọc nhận xét này qua blog, vì trang Hexagon Locaith tải chỉ có tóm tắt và danh sách tài liệu tham khảo, không có thân bài. Hai: bản thảo "The Unbalanced Group Theorem" (hexagon:2610.00575, bản 1, ngày 27/10, CC BY-4.0) là bản lưu tại Hexagon, không phải bài đã bình duyệt: trang Hexagon ghi nhận bài "không phải phán xét về tính đúng, chất lượng hay độ mới", mục DOI ghi "chưa gán", và người đóng góp là Colin Defant và Ken Ono, cũng là hai người trong danh sách đóng góp của dự án Axiom. Nhãn "chủ yếu do người viết" cũng có trên trang. Ngoài bản thảo, Axiom nói đã tham vấn Richard Lyons và Ronald Solomon, và sẽ tiếp tục xử lý errata cùng một hội đồng cố vấn nhà lý thuyết nhóm gồm hai người này.

Điều đáng rút ra cho người đang dùng tác tử

Đây là nhận xét của Locaith, không phải kết luận của Axiom. Khối lượng 43 triệu dòng chỉ làm được bằng đàn tác tử vì có một bộ kiểm cơ học rẻ, chặt và không thiên vị: kernel của Lean. Blog tự kể chỗ khó là phần Lean không kiểm được. Tác tử từng "giả định thay vì chứng minh" và phải xoá hàng chục nghìn dòng; một định lý chứng minh được với giả thiết thêm vẫn qua được nhân nhưng bỏ trống cột mốc; một định lý đúng nhưng khác phát biểu cần dùng cũng vậy. Axiom phải dựng lớp rà soát riêng cho chuyện này (đối chiếu phát biểu đã chứng minh với mục tiêu), và cuối cùng chuyển gánh nặng kiểm sang chính phát biểu cuối, thứ con người vẫn phải đọc.

Bài học thực dụng cho doanh nghiệp ở Việt Nam: công việc tác tử chỉ nên tự động chấp nhận ở nơi có kiểm tra cơ học rẻ và đúng mục tiêu (kiểm thử đơn vị đủ chặt, đối soát số liệu, định dạng bắt buộc); ở nơi còn lại, phần con người cần đọc là đặc tả (đề bài), không chỉ kết quả. Ở những việc không có "kernel của Lean" như vậy, người đọc đặc tả vẫn là khâu không thay được.

Giới hạn của bài này

Ngày 28/10/2026 Locaith đọc toàn bài blog Axiom, trang cfsg.axiommath.ai, README và formalization.yaml của kho, tệp phát biểu của TauCeti, trang giới thiệu và trang bản thảo của Hexagon, tệp lean_meta.json. Bốn nguồn thứ cấp (kingy.ai, Unite.AI, Crypto Briefing, Digg) Locaith đọc qua công cụ tóm tắt trang, không phải toàn văn, nên các câu gán cho chúng ở trên là cách hiểu của Locaith về phần tóm tắt. Lời của Vasily Ilin trên X Locaith chỉ lấy được phần đầu (bản trích của X bị cắt), phần "hàng trăm lỗi" lấy từ Digg. Blog đề ngày 26/10 còn mọi dấu vết khác (kho, bài đăng X, bản thảo Hexagon) là 27/10; Locaith không biết lý do chênh. Locaith không tìm thấy phản hồi công khai của Lyons, Solomon hay các tác giả CFSG gốc về công trình này, điều đó không có nghĩa là chưa có. Danh sách errata chưa được đăng trên trang khi Locaith xem.