Я завершил полную автоформализацию с @HarmonicMath Aristotle следующей задачи общей теории групп Задайте три положительных целых числа 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 строк кода на Lean. Теорему нельзя разрешить с помощью классических систем компьютерной алгебры. Она включает в себя предыдущую попытку с выбором n=m=k=2, сделанную ранее.