J'ai complété une auto-formalisation complète avec @HarmonicMath Aristotle du problème général de théorie des groupes suivant Fixez trois entiers positifs n, k, m. Prouvez qu'un sous-groupe H d'un groupe S_{6+(n+k+m)} généré par 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]>; satisfait H = S_{6+(n+k+m)} ou H = A_{6+(n+k+m)}. Nous avons H = S_{6+n+k+m} si et seulement si au moins un de n, k, m est pair, sinon H=A_{6+(n+k+m)}. Dépôt GitHub avec le code Lean et un croquis informel de ChatGPT-5.1-Pro L'auto-formalisation en deux courses mixtes (au total environ 20 heures). Le code contient environ 2600 lignes de code Lean. Le théorème ne peut pas être résolu avec des systèmes classiques d'algèbre informatique. Il englobe la tentative précédente avec les choix n=m=k=2 effectués auparavant.