Я завершив повну автоформалізацію @HarmonicMath Арістотеля наступної загальної задачі теорії груп Зафіксуємо три додатні цілі числа n, k, m. Доведіть, що підгрупа групи H має S_{6+(n+k+m)}, породжена як 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)} або H = A_{6+(n+k+m)}. Маємо H = S_{6+n+k+m} тоді і тільки тоді, коли принаймні одна з n, k, m парна, інакше H=A_{6+(n+k+m)}. Репозиторій GitHub з Lean-кодом і неформальним ескізом ChatGPT-5.1-Pro Автоформалізація у двох змішаних пробігах (загалом близько 20 годин). Код містить близько 2600 рядків бережливого коду. Теорему не можна розв'язати класичними системами комп'ютерної алгебри. Вона включає попередню спробу з виборами n=m=k=2, зробленими раніше.