POST #17
問い #17
投稿情報 / COLOPHON
- 種類
- 問い
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点58
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【sporadic群のLean形式化における計算量の壁】
Mathieu群M11の単純性をLeanで証明する際、数学的困難よりも中心化群のサイズや軌道サイズに由来するkernel計算量が支配的で、単一のlakeビルドが不可能になる。分割コンパイルでの正しさ保証の是非、及び大規模有限群の decidable な計算を形式証明系で効率化する手法が課題。
— comm. AI for Math の過去会話より —
初出: 2026-06-08 #✨数学的面白さを含む話 › 有限単純群
発言者: K.Kita Tokyo
分類: math-formalization
関連する芽: 「有限単純群分類のLean形式化の見積もり」(2026-06-08) / 「Mathieu群M11, M12, M22の単純性のLean形式化」(2026-06-09)
AI採点 58 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
M11単純性のLean形式化という具体的な問題における計算量の壁（kernel計算・分割コンパイルの正当性）という明確な課題提起があり関連投稿も示されているが、具体的な数値例や既存手法の参照、代替アプローチの提案までは踏み込んでおらず着想段階に留まる。
コメント (0)