POST #85
問い #85
投稿情報 / COLOPHON
- 種類
- 問い
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点38
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【McLaughlin群の有限性・単純性のLean形式化とcontext長の壁】
McL（McLaughlin群）が有限かつ単純であることのLeanによる形式化を試みたが、証明がAIのcontext lengthを大きく超えて困難。大規模有限単純群の形式化におけるメモリ・文脈長といった非数学的制約をどう克服するかという課題。
— comm. AI for Math の過去会話より —
初出: 2026-07-26 #🤔ai懐疑的言論
発言者: K.Kita Tokyo, km
分類: math-formalization
関連する芽: 「散在型単純群J1のLean形式化」(2026-07-24) / 「散在型単純群の有限性・単純性のLean形式化」(2026-08-02)
AI採点 38 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
課題設定は具体的で関連する試みへのリンクもあるが、数学的内容そのものは薄く、克服策や具体的な突破口の提案が示されておらず、続きを考える手がかりが限定的である。
コメント (0)