Axiom Math, một công ty xây dựng hệ thống AI cho toán học có trụ sở tại San Francisco, đã phát hành bằng chứng hoàn chỉnh đầu tiên được kiểm tra bằng máy tính về Phân loại nhóm đơn giản hữu hạn (CFSG), được mô tả rộng rãi là bằng chứng dài nhất trong lịch sử toán học. Theo thông báo của công ty, các kỹ sư và nhà toán học đã chỉ đạo hàng chục tác nhân AI chỉ trong 24 ngày để tạo ra khoảng 43,1 triệu dòng mã trong trợ lý chứng minh Lean, xác minh một kết quả trước đó trải dài khoảng 15.000 trang trên hơn 500 bài báo được viết bởi khoảng 100 nhà toán học trong nhiều thập kỷ.
Thành tựu này đạt được vào thời điểm toán học được máy hỗ trợ đang tăng tốc nhanh chóng và các cơ quan theo dõi tin tức nghiên cứu AI đã theo dõi quá trình xác minh chính thức chuyển từ thực tiễn thích hợp sang khả năng tiên tiến. Điều làm cho bản phát hành này trở nên khác thường là quy mô: quá trình chính thức hóa chứa khoảng 2,05 triệu khai báo được sắp xếp thành 100 cột mốc, mỗi cột mốc đó được kiểm tra bởi nhân của Lean, lõi nhỏ đáng tin cậy xác minh từng bước logic.
Phân loại thực sự nói lên điều gì
Các nhóm hữu hạn đơn giản là các khối xây dựng không thể chia cắt của tính đối xứng hữu hạn và sự phân loại - có biệt danh là "định lý khổng lồ" - đưa ra danh sách đầy đủ về chúng. Theo tài liệu của dự án, mọi nhóm đơn giản hữu hạn là một trong bốn loại: nhóm tuần hoàn có bậc nguyên tố, nhóm xen kẽ trên ít nhất năm ký hiệu, một trong mười sáu họ vô hạn của các nhóm loại Lie được xây dựng trên các trường hữu hạn hoặc một trong chính xác 26 nhóm rời rạc không thuộc họ nào.
Việc chứng minh rằng danh sách này đã sử dụng hết mọi khả năng đã mất hơn một thế kỷ nỗ lực tập thể. John Thompson, người có công trình đóng vai trò trung tâm trong phân loại, đã nhận được Huy chương Fields năm 1970 và Giải Abel năm 2008. Bằng chứng quá dài và được phân phối qua nhiều bài báo và nhiều thế hệ nhà toán học đến nỗi những nghi ngờ dai dẳng về tính hoàn chỉnh của nó vẫn tồn tại trong nhiều thập kỷ - những nghi ngờ về sự hình thức hóa này giờ đây đã chính thức bị xua tan.
Bầy đại lý trên 500 nguồn
Bằng chứng ban đầu nằm rải rác trên hơn 500 bài báo và sách, nhiều bài viết cách đây hàng chục năm với những ký hiệu không tương thích. Một kỹ sư của Axiom đã mô tả phương pháp này trong cuộc thảo luận của Hacker News về bản phát hành: một nhóm đặc vụ được giao nhiệm vụ xem xét tất cả các nguồn này, với phần khó khăn là tập hợp mọi thứ thành một tổng thể mạch lạc, vì cùng một khái niệm không chính thức có thể được chính thức hóa theo những cách hơi khác nhau nhưng không tương thích về mặt toán học.
Bài đăng trên blog của công ty cho biết nỗ lực này mất 24 ngày kể từ khi bắt đầu phát hành, với các kỹ sư và nhà toán học là con người chỉ đạo các nhóm đại lý thay vì làm việc theo từng dòng. Kết quả này tiếp nối các cột mốc tự động chính thức hóa cao cấp trước đó vào năm 2026, bao gồm các bằng chứng Lean về các định lý cổ điển chính được tạo ra bằng các mô hình biên giới, nhưng ở quy mô chưa có dự án nào trước đó đạt được.
34 sai lệch so với hồ sơ đã công bố
Việc dịch chứng minh đã công bố sang dạng có thể kiểm tra bằng máy đã bộc lộ những vấn đề thực tế trong tài liệu toán học. Axiom báo cáo rằng hầu hết các vấn đề đều nhỏ - lỗi đánh máy, lỗi trong bảng biểu hoặc bỏ sót giả thuyết. Tuy nhiên, có 34 sai lệch đáng chú ý so với hồ sơ đã công bố cần phải được giải quyết trước khi quá trình chính thức hóa được thực hiện.
Điều quan trọng nhất liên quan đến Định lý nhóm không cân bằng. Trong khi chính thức hóa lộ trình thế hệ đầu tiên dẫn đến kết quả, nhóm đã tìm thấy các phản ví dụ cho một xác nhận kết thúc được sử dụng trong một lập luận đã công bố. Với sự tham khảo ý kiến của các nhà lý thuyết nhóm chuyên gia, họ đã xây dựng một lộ trình thay thế được xây dựng dựa trên các kỹ thuật cấu trúc thời Daniel Gorenstein - cụ thể là lý thuyết về 2 thành phần cực đại từ những năm 1970 - và xuất bản bản sửa lỗi dưới dạng bài báo lý thuyết nhóm dài 35 trang mới, được đăng dưới dạng bản in sẵn 2610.00575. Công ty cho biết họ sẽ phát hành một danh sách dài các lỗi sai vì lợi ích của cộng đồng toán học, được biên soạn với sự tư vấn của các nhà lý thuyết nhóm phụ trách công việc phân loại.
Tại sao Toán học được kiểm tra bằng máy lại quan trọng
Giá trị của việc hình thức hóa không chỉ nằm ở chỗ máy tính đã phê duyệt bằng chứng. Việc chính thức hóa Lean làm giảm cơ sở tin cậy đối với cốt lõi của trợ lý chứng minh — một chương trình nhỏ, được kiểm toán chặt chẽ — thay vì độ tin cậy tích lũy của hàng nghìn trang được đọc bởi các chuyên gia rải rác. Những người bình luận trên chủ đề Hacker News, nơi câu chuyện đã thu hút hàng trăm lượt tán thành, lưu ý rằng kiến thức thực nghiệm về lý do tại sao cách phân loại này có nguy cơ bị lụi tàn theo đúng nghĩa đen khi thế hệ các nhà toán học ban đầu đã nghỉ hưu, bởi vì không một cá nhân nào có thể ghi nhớ toàn bộ lập luận đó trong đầu họ.
Cũng có những tiếng vang thực tế ở những nơi khác trong vật lý học. Nhóm lớn nhất trong số 26 nhóm lẻ tẻ, nhóm Quái vật, xuất hiện trong chương trình "ánh trăng quái dị" kết nối tính đối xứng hữu hạn với các hàm mô đun - công trình đã mang lại cho Richard Borcherds Huy chương Fields năm 1998 - và trong đề xuất năm 2007 của Edward Witten liên kết các đối xứng của Quái vật với entropy lỗ đen trong một vũ trụ ba chiều đơn giản hóa. Một phân loại đã được xác minh sẽ đặt cơ sở toán học cấu trúc cơ bản trên nền tảng vững chắc hơn cho các loại ứng dụng liên ngành này.
Điều gì xảy ra tiếp theo
Axiom cho biết nhiều tài liệu bắt nguồn từ quá trình chính thức hóa đang được triển khai cùng với dự án errata. Đối với cộng đồng các phương pháp chính thức, bản phát hành đặt ra một tiêu chuẩn mới cho những gì các dự án xác minh do tác nhân hướng dẫn có thể thử; đối với toán học, nó biến một thành tựu hợp tác kéo dài nửa thế kỷ thành một tạo tác duy nhất mà bất kỳ máy tính nào cũng có thể kiểm tra được. Việc phân loại không còn chỉ được tin tưởng nữa. Giờ đây, theo nghĩa đen nhất, nó đã được chứng minh — và bằng chứng có sẵn cho bất kỳ ai tải xuống và xác minh.
