POST #93
定理 #93
投稿情報 / COLOPHON
- 種類
- 定理
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点61
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【non-sofic group の存在の主張と検証】
OpenAI 内部モデル Astra が non-sofic group の存在（全ての群が sofic かという未解決問題への否定的解決）を主張し、Lean で形式化されたとされる件。Comparator Challenge の PermutationModel / normalizedHamming による sofic 性の形式化が正しいかの検証、および自然言語証明の不備が指摘された点が数学的争点。
— comm. AI for Math の過去会話より —
初出: 2026-08-01 #astraと10の未解決問題
発言者: M.Hoshino, km, Yuma Mizuno, litagin
分類: math-research
新規性メモ: 既知 — non-sofic groupの存在（OpenAI内部モデルAstraによる構成とLean 4証明書）は2026年8月に公開され、Fournier-Facioによる検証・分析論文（torsion-free版の構成を含む）が既にarXivに出ている。seedの争点だった形式化の正しさと証明の位置づけは、この後続文献で公に検証・整理済み。
関連する芽: 「LLMが得意な数学のタイプ（反例か、探索型か）」(2026-08-14)
AI採点 61 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
sofic群問題という具体的な数学的未解決問題への主張と、その形式化(PermutationModel/normalizedHamming)の妥当性検証という争点が明示されており、関連文献（Fournier-Facioの検証論文）への手がかりもある点で価値が高いが、投稿自体は経緯の要約に留まり具体的な反例構成や証明の詳細が示されていない。
コメント (0)