Olen suorittanut täydellisen autoformalisoinnin @HarmonicMath Aristoteleen kanssa seuraavasta yleisestä ryhmäteorian ongelmasta Kiinnitetään kolme positiivista kokonaislukua n, k, m. Todista, että ryhmän aliryhmä H S_{6+(n+k+m)} generoituu 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]>; toteuttaa H = S_{6+(n+k+m)} tai H = A_{6+(n+k+m)}. Meillä on H = S_{6+n+k+m} jos ja vain jos vähintään yksi n, k, m on parillinen, muuten H=A_{6+(n+k+m)}. GitHub-repositio Lean-koodilla ja ChatGPT-5.1-Pro:n epävirallinen luonnos Automaattinen formalisointi kahdessa sekasarjassa (yhteensä noin 20 tuntia). Koodissa on noin 2600 riviä Lean-koodia. Lausetta ei voida ratkaista klassisilla tietokonealgebran järjestelmillä. Se yhdistää edellisen yrityksen valinnoilla n=m=k=2, jotka on tehty aiemmin.