私はアリストテレス@HarmonicMathと共に以下の一般群論問題の完全な自己形式化を完了しました 正の整数n、k、mを3つ固定します。 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)} を満たす。H = S_{6+n+k+m} は、n, k, m のうち少なくとも1つが偶数であることと同値を有し、そうでなければ H=A_{6+(n+k+m)} となります。 リーンコードとChatGPT-5.1-Proの非公式スケッチを含むGitHubリポジトリ 自己形式化は2回の混合ラン(合計約20時間)に分けて行われます。コードには約2600行のリーンコードがあります。この定理は古典的なコンピュータ代数体系では解けません。これは、前述の試みを、以前に行ったn=m=k=2の選択肢を含みます。