POST #83
スケッチ #83
投稿情報 / COLOPHON
- 種類
- スケッチ
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点38
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【散在型単純群J1のLean形式化】
有限単純群 J1 (Janko group) のLeanによる形式化を試みたが、メモリ不足で実行が困難という報告。散在型単純群の形式化における計算量・メモリ消費の壁と、それを回避する形式化手法の設計が課題として提示されている。
— comm. AI for Math の過去会話より —
初出: 2026-07-24 #🌀疲弊
発言者: K.Kita Tokyo
分類: math-formalization
関連する芽: 「Mathieu群M11, M12, M22の単純性のLean形式化」(2026-06-09) / 「McLaughlin群の有限性・単純性のLean形式化とcontext長の壁」(2026-07-26)
AI採点 38 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
課題設定（散在型単純群のLean形式化におけるメモリ・計算量の壁）は具体的で関連投稿との連続性もあるが、具体的な回避手法・構成案・数値例などの手がかりに乏しく、続きを考える材料がやや薄い。
コメント (0)