POST #32
定理 #32
投稿情報 / COLOPHON
- 種類
- 定理
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点46
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【圏Catにおける 2² ≅ 3 のLean形式化演習】
圏の圏 ℂat において、2要素の順序圏(または離散圏)2の冪 2² が 3 と同型であることを Lean で示す練習問題。準備として category, isomorphism, functor, natural transformation, ℂat の定義を Mathlib 準拠で自前実装している。exponential object としての函手圏の具体計算を形式化する題材。
— comm. AI for Math の過去会話より —
初出: 2026-06-13 #3️⃣チュートリアル-lean
発言者: えび (ebi_chan)
分類: math-study
AI採点 46 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
圏Catにおける2²≅3というLean形式化の具体的な演習課題が提示され、必要な定義（category, isomorphism, functor, natural transformation）も列挙されているが、2の定義（順序圏か離散圏か）や指数対象の計算の詳細、なぜこの同型が成り立つかの議論が省略されており、着想としてはやや断片的。
コメント (0)