Aşağıdaki genel grup teorisi probleminin @HarmonicMath Aristoteles ile tam otomatik biçimselleştirmesini tamamladım Üç pozitif tam sayı n, k, m sabitleyin. S_{6+(n+k+m)}'nin bir grup alt grubu H'nin oluşturulduğunu kanıtlayın 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]>; H = S_{6+(n+k+m)} veya H = A_{6+(n+k+m)} sağlar. H = S_{6+n+k+m} ancak ve ancak en az biri n, k, m'nin çift olduğu durumlarda, aksi takdirde H=A_{6+(n+k+m)} durumunda elde ederiz. Lean kodu ve ChatGPT-5.1-Pro gayri resmi taslağı içeren GitHub deposu Otomatik resmileştirme iki karışık koşu içinde (toplamda yaklaşık 20 saat) gerçekleşti. Kodda yaklaşık 2600 satır Lean kodu var. Teorem klasik bilgisayar cebiri sistemleriyle çözülemez. Önceki denemeyi, önceki seçimlerle birlikte n=m=k=2 ile birleştirir.