我已经与 @HarmonicMath Aristotle 完成了以下一般群论问题的完整自动形式化。 固定三个正整数 n, k, m。 证明 S_{6+(n+k+m)} 的一个群子群 H 由以下生成： 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)}。当且仅当 n, k, m 中至少有一个是偶数时，H = S_{6+n+k+m}，否则 H=A_{6+(n+k+m)}。 包含 Lean 代码和 ChatGPT-5.1-Pro 非正式草图的 GitHub 仓库。 在两次混合运行中进行了自动形式化（总共约 20 小时）。代码大约有 2600 行 Lean 代码。该定理无法通过经典计算机代数系统解决。它包含了之前选择 n=m=k=2 的尝试。