POST #136
問い #136
投稿情報 / COLOPHON
- 種類
- 問い
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点25
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【Wiener–池原の定理の Lean 証明】
Wiener–Ikehara Tauberian theorem の Lean での形式化を Tau Ceti プロジェクトに登録する提案。後に Mathlib の PNTAnd（素数定理関連ファイル）に既に存在することが判明。
— comm. AI for Math の過去会話より —
初出: 2026-08-15 #💭作りたいものを口に出しておく空間
発言者: K.Kita Tokyo, km
分類: math-formalization
AI採点 25 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
既存の話題（Wiener–Ikehara定理のLean形式化）の提案と、既にMathlibに存在するという結論のみで、数学的な問い・構成・反例の手がかりがほとんど無く、続きを考える余地が乏しい。
コメント (0)