POST #99
スケッチ #99
投稿情報 / COLOPHON
- 種類
- スケッチ
- 数学分野
- 未設定
- 言語
- ja
- AI採点
- AI採点32
- 総合評価
- 未評価
- 調査
- 0件
- コメント
- 0件
【GapCVP の Lean 形式化が PCP 定理を回避する構成】
格子暗号の GapCVP に関する結果の Lean 形式化では Lean CSLib が存在しないため 13 万行超のコードでアルゴリズム的枠組みを Turing machine のビットレベルまで還元し、しかも PCP 定理を経由せずに hardness を導いているとの指摘。PCP を回避する証明手法自体が独立した研究対象となりうる。
— comm. AI for Math の過去会話より —
初出: 2026-08-02 #astraと10の未解決問題
発言者: km
分類: math-research
新規性メモ: 既知の可能性大 — PCP 定理を black box として経由しない lattice 問題の hardness 証明は既存文献にある（Dinur–Kindler–Raz–Safra の CVP hardness、および PCP を回避する最近の SVP 系の証明）。Lean 形式化に固有の還元構成が独立の新規手法かは専門的精査なしに断定できない。
AI採点 32 / 100 の理由を読む
AIがweb検索と本文から自動生成した、人の検証を経ていない採点です。投稿そのものの確定した評価ではありません。 採点したモデル: claude-sonnet-5
PCP定理を経由しないGapCVP困難性証明という着想は具体的で文献的手がかり（Dinur–Kindler–Raz–Safra等）もあるが、Lean形式化の詳細や還元構成そのものは示されておらず、続きを考えるための具体的な定義・構成が乏しい。
コメント (0)