Định lý phân loại nhóm đơn hữu hạn được hình thức hóa bằng Lean

Một dự án hình thức hóa toán học bằng ngôn ngữ Lean đã đạt bước tiến đáng chú ý khi hướng tới việc chứng minh trọn vẹn Định lý phân loại nhóm đơn hữu hạn (Classification of Finite Simple Groups – CFSG), một trong những kết quả đồ sộ và phức tạp nhất của toán học hiện đại. Quá trình này không chỉ kiểm chứng lại các chứng minh đã có mà còn dẫn tới một kết quả lý thuyết nhóm mới, được công bố trong bài báo The Unbalanced Group Theorem dài 35 trang.

Vì sao CFSG là một thử thách khổng lồ

Định lý phân loại nhóm đơn hữu hạn được xem là "bộ xương sống" của đại số hiện đại, với chứng minh gốc trải dài hàng chục nghìn trang trên nhiều tạp chí và mất hàng thập kỷ để hoàn thiện.

• Chứng minh truyền thống được viết bởi nhiều nhóm tác giả qua nhiều thế hệ, khiến việc kiểm tra tính đúng đắn trở nên cực kỳ khó khăn.
• Việc hình thức hóa bằng máy tính giúp loại bỏ sai sót do con người và tạo ra nền tảng có thể kiểm chứng tự động.

Việc chuyển toàn bộ chứng minh sang Lean — một trợ lý chứng minh tương tác — là nỗ lực tương đương với việc xây dựng lại một phần nền tảng toán học từ đầu, với từng bước suy luận đều phải được máy tính xác nhận.

Phát hiện phản ví dụ trong quá trình hình thức hóa

Điểm đáng chú ý nhất của dự án là trong khi hình thức hóa chứng minh "thế hệ thứ nhất", nhóm nghiên cứu đã tìm ra phản ví dụ cho một khẳng định đóng (closure assertion) từng được sử dụng trong một lộ trình đã công bố để chứng minh Định lý nhóm không cân bằng (Unbalanced Group Theorem).

Bài báo giải thích trở ngại này và đưa ra một lập luận thay thế cho trường hợp nhóm đơn, được xây dựng dựa trên lý thuyết về các 2-thành phần cực đại (maximal 2-components) của Solomon công bố năm 1976.

Bước then chốt trong lập luận mới là Định lý 2.3, về việc bảo toàn các "đỉnh đơn" (simple tops). Đây là minh chứng cho giá trị thực tiễn của hình thức hóa: quá trình kiểm tra chặt chẽ từng bước logic không chỉ xác nhận mà còn có thể phát hiện lỗ hổng trong các chứng minh đã được chấp nhận.

Ý nghĩa với cộng đồng công nghệ và toán học

Sự kiện này phản ánh xu hướng ngày càng mạnh mẽ của việc ứng dụng trợ lý chứng minh hình thức trong nghiên cứu toán học và khoa học máy tính.

• Lean và các thư viện như Mathlib đang trở thành hạ tầng quan trọng cho toán học có thể kiểm chứng bằng máy.
• Các dự án kiểu này đòi hỏi sự kết hợp giữa chuyên môn toán học sâu và kỹ năng lập trình, mở ra hướng đi mới cho các nhà nghiên cứu trẻ.
• Kết quả hình thức hóa có thể được tái sử dụng, mở rộng và kiểm chứng độc lập bởi bất kỳ ai, khác với các chứng minh trên giấy truyền thống.

Với cộng đồng công nghệ, đây là lời nhắc rằng các công cụ hình thức hóa không còn chỉ phục vụ kiểm chứng phần mềm mà đang vươn tới những đỉnh cao nhất của toán học thuần túy. Bạn có thể đọc thêm về kết quả này tại cfsg.axiommath.ai và thảo luận trên Hacker News.