proof-writer

proof-writer：数学証明執筆スキル

概要

本スキルは、学術論文における数学証明の執筆に特化しています。主張の抽出、戦略の選択から、完全な LaTeX 組版までのエンドツーエンドのワークフローをカバーします。説明はすべて繁体字中国語で行い、数学表現と LaTeX コードは英語を使用します。

---

ワークフローの概要

証明の執筆は、次の五つの段階を順に実行します。

主張提取 → 文獻掃描 → 策略選擇 → 逐步推導 → LaTeX 排版

各段階には、明確な入力、出力、品質チェックポイントがあります。以下で順に説明します。

---

第一段階：主張の抽出

目的

論文の草稿またはユーザーの入力から、証明が必要な数学的主張を正確に抽出します。主張は形式的な命題であり、 明確な前提条件と結論を備えている必要があります。

手順

1. 主張の種類を特定する：定理（Theorem）、補題（Lemma）、系（Corollary）、 命題（Proposition）、または主張（Claim）のいずれかを判断します。
2. 前提条件を抽出する：すべての仮定、制約条件、適用範囲を列挙します。
3. 結論を抽出する：証明すべき等式、不等式、または性質を明確に記述します。
4. 記号を確認する：すべての記号の定義と範囲を確認し、 記号の慣例を参照します。
5. 形式的に記述する：主張を標準的な数学の記述形式で記述します。

出力形式

主張類型：[Theorem | Lemma | Corollary | Proposition | Claim]
前提條件：
  - 條件 1
  - 條件 2
  - ...
結論：[形式化的數學陳述]
相關符號：[符號清單及定義]

よくある問題

• 前提条件が不完全：論文の仮定に関する段落を再確認します。
• 記号が未定義：論文の記法セクションを確認するか、ユーザーに確認します。
• 主張が曖昧すぎる：より正確な形式的記述をユーザーに求めます。

品質チェック

• 主張は判定可能な数学命題ですか？
• すべての記号は定義されていますか？
• 前提条件は結論を導くのに十分ですか？
• 主張の種類は正しく分類されていますか？

---

第二段階：文献調査

目的

主張に関連する既知の定理、補題、結果を調べ、証明の基盤を築きます。この段階によって、 「巨人の肩の上に立つ」ために利用できるものが決まります。

手順

1. キーワードを抽出する：主張から数学的なキーワード（例：収束、上界、 集中不等式など）を抽出します。
2. 定理を照合する：既知の定理のライブラリから関連する結果を検索し、 定理の関連付け方法を参照します。
3. 関連性を評価する：見つかった各定理と現在の主張との関連性を評価します。
4. 依存関係を確立する：どの定理をそのまま使えるか、どの定理に適度な修正が必要かを判断します。
5. ギャップを分析する：既知の結果と目標とする主張との間にある隔たりを特定します。

よく使われる定理の出典

• 論文の前半ですでに証明されている補題
• 論文で引用されている参考文献
• 分野の古典的な結果（Cauchy-Schwarz、Jensen's inequality など）
• 標準的な教科書に記載されている基本定理

出力形式

相關定理：
  1. [定理名稱] — [簡述] — 相關度：[高|中|低]
  2. ...
可直接引用：[定理列表]
需要修改後使用：[定理列表及修改方向]
證明缺口：[需要自行推導的部分]

品質チェック

• 重要な既知の結果を見落としていませんか？
• 引用した定理の前提条件は満たされていますか？
• 定理のバージョンは正しいですか（定理によっては複数の変形が存在します）？

---

第三段階：戦略の選択

目的

主張の構造と利用可能な既知の結果に基づいて、最も適切な証明戦略を選びます。戦略の選択は、 証明の明瞭さと長さに直接影響します。

利用可能な戦略

本スキルは以下の八つの証明戦略をサポートします。各戦略の詳細については、 証明戦略のリファレンスを参照してください。

1. 直接証明（Direct Proof）

前提条件から出発し、一連の論理的な推論を通じて結論に直接到達します。構造が明確で、推論の道筋が はっきりしている主張に適しています。

適用場面：等式の証明、不等式の導出、集合の包含関係。

2. 背理法（Proof by Contradiction）

結論が成り立たないと仮定し、矛盾を導きます。直接証明が難しい場合や、結論が否定形の主張に適しています。

適用場面：存在性の否定、一意性の証明、不可能性の結果。

3. 数学的帰納法（Mathematical Induction）

自然数または整列可能な構造に対して帰納法を行います。弱い帰納法、強い帰納法、構造帰納法を含みます。

適用場面：再帰的な構造、数列の性質、離散数学の命題。

4. 構成的証明（Constructive Proof）

条件を満たす対象を明示的に構成し、存在性を証明します。単なる存在証明よりも多くの情報が得られます。

適用場面：存在命題、アルゴリズムの正しさ、具体的な境界の導出。

5. 帰着法（Proof by Reduction）

証明すべき問題を既知の問題に帰着します。計算複雑性や決定問題でよく使われます。

適用場面：NP-hardness の証明、下界の証明、同値性の証明。

6. 確率的方法（Probabilistic Method）

条件を満たす対象がランダムな選択によって得られる確率が正であることを証明し、条件を満たす対象の存在を示します。

適用場面：組合せ数学、グラフ理論、ランダム化アルゴリズムの解析。

7. 凸性による議論（Convexity Arguments）

凸関数や凸集合の性質を利用して推論します。最適化や機械学習理論で特によく使われます。

適用場面：最適化問題、Jensen's inequality の適用、凸緩和。

8. 情報理論的手法（Information-theoretic Methods）

エントロピー、相互情報量、KL ダイバージェンスなどの情報理論のツールを使用して推論します。

適用場面：通信理論、学習理論の下界、プライバシー分析。

戦略選択の決定木

主張結構分析
├─ 等式或不等式？
│  ├─ 是 → 考慮直接證明、凸性論證
│  └─ 否 → 繼續
├─ 存在性命題？
│  ├─ 是 → 考慮構造性證明、機率法
│  └─ 否 → 繼續
├─ 涉及遞迴或序列？
│  ├─ 是 → 考慮數學歸納法
│  └─ 否 → 繼續
├─ 可歸約為已知問題？
│  ├─ 是 → 考慮歸約法
│  └─ 否 → 繼續
├─ 涉及資訊量度？
│  ├─ 是 → 考慮資訊論方法
│  └─ 否 → 繼續
└─ 直接證明困難？
   ├─ 是 → 考慮反證法
   └─ 否 → 使用直接證明

複合戦略

複雑な証明の多くでは、複数の戦略を組み合わせる必要があります。よくある組み合わせは次のとおりです。

• 帰納法 + 直接証明：帰納ステップで直接証明を用いる
• 背理法 + 構成的証明：存在しないと仮定し、矛盾する対象を構成する
• 帰着法 + 情報理論：情報理論の問題に帰着した後、情報理論のツールを用いる

出力形式

選擇策略：[主要策略名稱]
輔助策略：[如有]
選擇理由：[為什麼這個策略最適合]
預期證明結構：[大綱]
預期難度：[低|中|高]

---

第四段階：段階的な導出

目的

選択した戦略に基づいて、完全かつ厳密な証明を記述します。各ステップには明確な論理的根拠が必要です。

原則

1. 完全性：自明でないステップを省略しません。
2. 厳密性：各推論ステップには明確な数学的根拠が必要です。
3. 可読性：明瞭な言葉で読者を導きます。
4. モジュール性：複雑な証明は複数の補題に分割します。

執筆規則

推論ステップの形式

各推論ステップには以下を含めます。

• 記述：このステップで確立する中間結論
• 導出：具体的な数学的導出過程
• 根拠：引用する定理、補題、または先行するステップ

接続表現

ステップ間では適切な接続表現を使い、証明の論理的な流れが読者に伝わるようにします。

• 「仮定より、……」
• 「定理 X より、……が従います。」
• 「（1）と（2）を組み合わせると、……が得られます。」
• 「一般性を失うことなく、……」
• 「……の定義より、……が成り立ちます。」

よくある注意点

• ステップを省略するために「明らかに」、「自明に」、「簡単に」などの表現を使わないでください。
• あるステップの導出に三行を超える場合は、独立した補題として取り出すことを検討してください。
• すべての変数が使用前に定義されていることを確認してください。
• 量化子（すべてについて、あるものが存在する）の作用域が明確であることを確認してください。

品質チェック

• 各推論ステップに明確な論理的根拠がありますか？
• 説明されていない仮定はありませんか？
• 量化子は正しく使われていますか？
• 記号は論文の他の部分と一致していますか？
• 証明は完全ですか（QED または $\square$ で終わっていますか）？

---

第五段階：LaTeX 組版

目的

証明を論文にそのまま挿入できる LaTeX コードに変換します。組版は学術論文の標準的な形式に従う必要があります。

組版規則

LaTeX 組版パターンの詳細については、LaTeX 数式組版のリファレンスを参照してください。

基本環境

\begin{theorem}[Theorem Name]
\label{thm:theorem-label}
  Statement of the theorem.
\end{theorem}

\begin{proof}
  Proof content here. \qed
\end{proof}

番号付けと参照

• すべての定理、補題、系に \label を付けます。
• 相互参照には \ref または \eqref を使用します。
• 数式の番号付けには equation または align 環境を使用します。

組版スタイル

• インライン数式には $...$ を使用します。
• 別行立ての数式には \[...\] または番号付きの環境を使用します。
• 複数行の整列には align 環境を使用します。
• 場合分けには cases 環境を使用します。

出力形式

最終的な出力には、以下を含めます。

1. 完全な LaTeX コードスニペット（そのままコピーして貼り付けられます）
2. 必要な追加パッケージの一覧（amsthm、amsmath など）
3. カスタムコマンドが必要な場合は、\newcommand の定義

品質チェック

• LaTeX コードは正常にコンパイルできますか？
• 数学記号は正しく表示されますか？
• 番号付けと参照は正しいですか？
• 組版は見やすいですか（整列、間隔など）？
• 対象とするジャーナルの書式要件に準拠していますか？

---

符號與排版參考

• 證明策略詳細說明
• 定理連結方法
• 符號慣例
• LaTeX 數學排版模式

---

使用範例

範例一：簡單不等式證明

輸入：證明對所有 $x > 0$，有 $e^x \geq 1 + x$。

第一階段輸出：

主張類型：Proposition
前提條件：
  - x > 0, x ∈ ℝ
結論：e^x ≥ 1 + x
相關符號：e 為自然對數的底

第三階段輸出：

選擇策略：直接證明
選擇理由：可通過分析 f(x) = e^x - 1 - x 的性質直接推導
預期證明結構：
  1. 定義 f(x) = e^x - 1 - x
  2. 計算 f'(x) = e^x - 1
  3. 分析 f 的單調性
  4. 利用 f(0) = 0 得出結論
預期難度：低

第五階段輸出：

\begin{proposition}
\label{prop:exp-lower-bound}
  For all $x > 0$, we have $e^x \geq 1 + x$.
\end{proposition}

\begin{proof}
  Define $f(x) = e^x - 1 - x$. We have $f(0) = 0$ and
  $f'(x) = e^x - 1 > 0$ for all $x > 0$. Therefore, $f$ is
  strictly increasing on $(0, \infty)$, which implies
  $f(x) > f(0) = 0$ for all $x > 0$. That is, $e^x > 1 + x$.
  \qed
\end{proof}

範例二：機器學習中的泛化界

輸入：證明 PAC learning 框架下，有限假設類的樣本複雜度上界。

第一階段輸出：

主張類型：Theorem
前提條件：
  - H 為有限假設類，|H| < ∞
  - 樣本 S 由分布 D 上的 m 個 i.i.d. 樣本組成
  - ε > 0, δ > 0
結論：若 m ≥ (1/ε)(ln|H| + ln(1/δ))，則以機率至少 1-δ，
      對所有 h ∈ H 有 |R(h) - R̂(h)| ≤ ε
相關符號：R(h) 為真實風險，R̂(h) 為經驗風險

第三階段輸出：

選擇策略：直接證明 + 機率法
輔助策略：歸約到 Hoeffding's inequality
選擇理由：經典的 union bound + concentration inequality 組合
預期證明結構：
  1. 對單一假設 h 應用 Hoeffding's inequality
  2. 對所有假設取 union bound
  3. 解出 m 的下界
預期難度：中

---

常見工作模式

模式一：完整證明撰寫

用戶提供主張，系統執行完整的五階段流程，輸出可直接使用的 LaTeX 代碼。

模式二：證明修復

用戶提供有問題的證明，系統診斷問題所在並修復。常見問題包括：

• 邏輯跳躍（缺少中間步驟）
• 量詞錯誤
• 邊界情況未處理
• 引用的定理前提條件不滿足

模式三：證明翻譯

將非形式化的直覺論證轉換為嚴謹的數學證明。

模式四：策略諮詢

用戶描述要證明的目標，系統建議可能的證明策略和思路，但不撰寫完整證明。

---

注意事項

1. 嚴謹性優先：寧可冗長也不要跳步。讀者可以略過顯然的步驟，但無法填補 缺失的步驟。
2. 符號一致性：所有符號必須與論文其餘部分一致。如有衝突，在證明開頭明確 說明。參照 符號慣例。
3. 可編譯性：輸出的 LaTeX 必須可以直接編譯，不能有語法錯誤。
4. 學術語調：使用正式的學術英文撰寫數學部分，避免口語化表達。
5. 引用規範：使用的所有非本文證明的結果，都必須提供引用。