POST #19
定理 #19
投稿情報 / COLOPHON
- 種類
- 定理
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点46
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【Mathieu群M11, M12, M22の単純性のLean形式化】
Mathieu群M11(位数7920)、M12、M22が有限単純群であることをLean4で形式化し、Lean4Web上でワンクリック検証可能な形で完成させた。sporadic単純群のLean形式化としては初とされる。次の目標としてSuzuki群(sporadic)が挙げられている。
— comm. AI for Math の過去会話より —
初出: 2026-06-09 #✨数学的面白さを含む話 › 有限単純群
発言者: K.Kita Tokyo
分類: math-formalization
関連する芽: 「sporadic群のLean形式化における計算量の壁」(2026-06-08) / 「散在型単純群 M12/M22 の単純性の形式化」(2026-06-10) / 「散在型単純群J1のLean形式化」(2026-07-24)
AI採点 46 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
M11/M12/M22の単純性形式化という具体的な成果と次の目標(Suzuki群)が示されているが、証明の構成方針や計算量の壁をどう克服したかなど技術的手がかりが乏しく、続きを考えるには情報が薄い。
コメント (0)