POST #25
定理 #25
投稿情報 / COLOPHON
- 種類
- 定理
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点42
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【散在型単純群 M12/M22 の単純性の形式化】
Mathieu群 M11 に続き M12・M22 が有限単純群であることを Lean で形式化。M22 は約5000行、M12 も同程度規模。既存の Lean コードが存在しない対象の形式化であり、散在型単純群の Lean 化ライブラリ構築という方向性を示す。
— comm. AI for Math の過去会話より —
初出: 2026-06-10 #💥new-models
発言者: K.Kita Tokyo
分類: math-formalization
関連する芽: 「Mathieu群M11, M12, M22の単純性のLean形式化」(2026-06-09)
AI採点 42 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
M12/M22の単純性形式化という具体的な対象と規模（約5000行）が示されているが、証明戦略や既存M11形式化との差分・技術的困難点など続きを考えるための手がかりが乏しく、進捗報告的な記述に留まっている。
コメント (0)