Jag har slutfört en fullständig autoformalisering med @HarmonicMath Aristoteles av följande allmänna gruppteoriproblem Fixera tre positiva heltal n, k, m. Bevisa att en gruppdelgrupp H av S_{6+(n+k+m)} genereras av 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]>; uppfyller H = S_{6+(n+k+m)} eller H = A_{6+(n+k+m)}. Vi har H = S_{6+n+k+m} om och endast om minst en av n, k, m är jämn, annars H=A_{6+(n+k+m)}. GitHub-repo med Lean-kod och ChatGPT-5.1-Pro informell skiss Autoformaliseringen var i två blandade omgångar (totalt cirka 20 timmar). Koden har cirka 2600 rader Lean-kod. Satsen kan inte lösas med klassiska datoralgebrasystem. Den underordnar det föregående försöket med de val n=m=k=2 som gjorts tidigare.