POST #94
問い #94
投稿情報 / COLOPHON
- 種類
- 問い
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点30
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【Connes' rigidity conjecture の Lean 形式化の依存関係監査】
ConnesRigidity.lean において、最終定理を仮定に置いていないか、sorry/独自 axiom がないか、universal lattice の property (T) が内部で証明されているか、Suslin 型生成定理の必要な特殊ケースが証明されているか、因子同型の explicit witness が構成されているか、といった依存関係の監査項目が整理された。
— comm. AI for Math の過去会話より —
初出: 2026-08-01 #astraと10の未解決問題
発言者: Yasu, km, Qu, M.Hoshino
分類: math-formalization
AI採点 30 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
監査項目のリスト自体は具体的だが、実際の定理・証明内容や反例・文献への言及がなく、Lean形式化の中身自体は示されていないため、続きを考える手がかりが限定的である。
コメント (0)