Saya telah menyelesaikan formalisasi otomatis penuh dengan @HarmonicMath Aristoteles tentang masalah teori kelompok umum berikut Perbaiki tiga bilangan bulat positif n, k, m. Buktikan bahwa subgrup grup H dari S_{6+(n+k+m)} dihasilkan oleh 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]>; memenuhi H = S_{6+(n+k+m)} atau H = A_{6+(n+k+m)}. Kita memiliki H = S_{6+n+k+m} jika dan hanya jika setidaknya salah satu dari n, k, m genap, jika tidak, H=A_{6+(n+k+m)}. Repo GitHub dengan kode Lean dan sketsa informal ChatGPT-5.1-Pro Formalisasi otomatis dalam dua proses campuran (seluruhnya sekitar 20 jam). Kode ini memiliki sekitar 2600 baris kode Lean. Teorema tidak dapat diselesaikan dengan sistem aljabar komputer klasik. Ini menggabungkan upaya sebelumnya dengan pilihan n=m=k=2 yang dilakukan sebelumnya.