Một nhóm nhà toán học và kỹ sư vừa công bố bản chứng minh hình thức hoàn chỉnh cho định lý phân loại các nhóm đơn hữu hạn, được máy tính kiểm tra từng bước bằng Lean, một phần mềm chứng minh định lý. Dự án do Axiom Math dẫn dắt, có sự tham gia của nhiều tên tuổi như Ken Ono và Colin Defant.

Một trong những thành tựu lớn nhất của toán học

Định lý phân loại là một thành tựu tập thể lớn của toán học. Định lý khẳng định mọi nhóm đơn hữu hạn thuộc một trong bốn loại: nhóm xyclic bậc nguyên tố, nhóm thay phiên, nhóm kiểu Lie, hoặc một trong 26 nhóm rời rạc. Bản chứng minh gốc dài hàng nghìn trang tạp chí, do khoảng một trăm nhà toán học viết trong nhiều thập kỷ, nên rất khó để một người kiểm tra trọn vẹn.

Phát hiện lỗi trong tài liệu đã công bố

Trong quá trình số hóa, nhóm nghiên cứu tìm thấy phản ví dụ cho một khẳng định trong lập luận đã đăng về Định lý Nhóm Không Cân Bằng. Họ đề xuất hướng chứng minh thay thế dựa trên lý thuyết của Solomon từ năm 1976 và đang cùng các chuyên gia lý thuyết nhóm tổng hợp danh sách errata.

Vì sao điều này quan trọng

Đây là minh chứng cho thấy AI và công cụ kiểm chứng có thể giúp con người rà soát những công trình khổng lồ mà trước đây gần như không ai đọc hết. Với giới công nghệ, đó là bước tiến cho việc xây dựng phần mềm và hệ thống đáng tin cậy hơn.

#Chứng minh hình thức

Axiom hoàn tất chứng minh phân loại nhóm đơn hữu hạn bằng Lean