Tôi đã hoàn thành một quá trình tự động hóa hoàn toàn với @HarmonicMath Aristotle về bài toán lý thuyết nhóm tổng quát sau đây Cố định ba số nguyên dương n, k, m. Chứng minh rằng một nhóm con H của S_{6+(n+k+m)} được sinh ra bởi g1:=G!(1,6,4,3,a_1,...a_n); g2:=G!(1,2,4,5,b_1,...,b_k); g3:=G!(5,6,2,3,c_1,...,c_m); H:=sub<G|[g1,g2,g3]>; thỏa mãn H = S_{6+(n+k+m)} hoặc H = A_{6+(n+k+m)}. Chúng ta có H = S_{6+n+k+m} nếu và chỉ nếu ít nhất một trong các n, k, m là số chẵn, nếu không H=A_{6+(n+k+m)}. Kho lưu trữ GitHub với mã Lean và phác thảo không chính thức ChatGPT-5.1-Pro Quá trình tự động hóa trong hai lần chạy hỗn hợp (tổng cộng khoảng 20 giờ). Mã có khoảng 2600 dòng mã Lean. Định lý này không thể được giải quyết bằng các hệ thống đại số máy tính cổ điển. Nó bao hàm nỗ lực trước đó với các lựa chọn n=m=k=2 đã thực hiện trước đó.