Dokončil jsem s Aristotelem úplnou autoformaliz@HarmonicMath aci následujícího obecného problému teorie grup Určme tři kladná celá čísla n, k, m. Dokažte, že podgrupa H S_{6+(n+k+m)} generovaná 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]>; Vyhovuje H = S_{6+(n+k+m)} nebo H = A_{6+(n+k+m)}. Máme H = S_{6+n+k+m} právě tehdy, když alespoň jeden z n, k, m je sudý, jinak H=A_{6+(n+k+m)}. GitHub repozitář s Lean kódem a neformální skicou ChatGPT-5.1-Pro Autoformalizace ve dvou smíšených běhech (celkem asi 20 hodin). Kód obsahuje přibližně 2600 řádků Lean kódu. Větu nelze vyřešit klasickými systémy počítačové algebry. Zahrnuje předchozí pokus s volbami n=m=k=2 provedenými dříve.