POST #114
問い #114
投稿情報 / COLOPHON
- 種類
- 問い
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点58
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【巨大置換群の証明分割：良い安定化鎖・部分群構造の探索】
Lean の証明検査は空間計算量に実質上限があるため、巨大な計算を小さな証明証明書に分割する必要がある。機械的分割では不十分で、計算量を落とす良い stabilizer chain / 部分群構造を数学的に見つけることがボトルネック。Fi23, Co1, ON は適切な分割で到達可能と予想され、Th のように置換次数自体が爆発する群には巨大置換を直接検査しない新しい分解手法が必要。
— comm. AI for Math の過去会話より —
初出: 2026-08-05 #🪻lean-proofs
発言者: K.Kita Tokyo, M.Hoshino, hitsujikaip
分類: math-formalization
関連する芽: 「散在型単純群の有限性・単純性のLean形式化」(2026-08-02)
AI採点 58 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
巨大置換群のLean検証における安定化鎖分割という具体的な問題設定と、Fi23/Co1/ON/Thでの難易度差など手がかりはあるが、数学的構成や候補となる分解手法の詳細が乏しく、続きを考えるにはやや情報不足。
コメント (0)