Am finalizat o auto-formalizare completă cu @HarmonicMath Aristotel a următoarei probleme generale de teorie a grupurilor Fixăm trei întregi pozitivi n, k, m. Demonstrează că un subgrup de grup H al S_{6+(n+k+m)} generat de 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]>; satisface H = S_{6+(n+k+m)} sau H = A_{6+(n+k+m)}. Avem H = S_{6+n+k+m} dacă și numai dacă cel puțin unul dintre n, k, m este par, altfel H=A_{6+(n+k+m)}. Repository GitHub cu cod Lean și schiță informală ChatGPT-5.1-Pro Auto-formalizarea în două serii mixte (în total aproximativ 20 de ore). Codul are aproximativ 2600 de linii de cod Lean. Teorema nu poate fi rezolvată cu sisteme clasice de algebră computațională. Aceasta încorporează încercarea anterioară cu alegerile n=m=k=2 făcute anterior.