Proof Writer

proof-writer：數學證明撰寫技能

概述

本技能專注於學術論文中的數學證明撰寫。涵蓋從主張提取、策略選擇到完整 LaTeX 排版的端對端工作流程。所有解釋使用繁體中文，數學表達式與 LaTeX 代碼使用英文。

流程總覽

證明撰寫分為五個階段，依序執行：

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

每個階段有明確的輸入、輸出與品質檢查點。以下逐一說明。

第一階段：主張提取

目的

從論文草稿或用戶輸入中，精確提取需要證明的數學主張。主張必須是形式化的命題， 具備明確的前提條件與結論。

步驟

1. 辨識主張類型：判斷是定理 (Theorem)、引理 (Lemma)、推論 (Corollary)、 命題 (Proposition)，還是聲明 (Claim)。
2. 提取前提條件：列出所有假設、約束條件與適用範圍。
3. 提取結論：明確寫出要證明的等式、不等式或性質。
4. 符號確認：確認所有符號的定義與範圍，參照 符號慣例。
5. 形式化陳述：將主張寫成標準的數學陳述格式。

輸出格式

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

常見問題

• 前提條件不完整：回頭檢查論文中的假設段落。
• 符號未定義：查閱論文的 notation section 或向用戶確認。
• 主張過於模糊：要求用戶提供更精確的形式化陳述。

品質檢查

• 主張是否為可判定的數學命題？
• 所有符號是否已定義？
• 前提條件是否足以推導結論？
• 主張類型是否正確分類？

第二階段：文獻掃描

目的

查找與主張相關的已知定理、引理和結果，為證明建立基礎。這一步決定了我們可以 「站在哪些巨人的肩膀上」。

步驟

1. 關鍵詞提取：從主張中提取數學關鍵詞（如 convergence、bound、 concentration inequality 等）。
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. 模組化：複雜的證明應拆分為多個引理。

撰寫規範

推導步驟格式

每一步推導應包含：

• 陳述：本步驟要建立的中間結論
• 推導：具體的數學推導過程
• 依據：引用的定理、引理或之前的步驟

過渡語句

在步驟之間使用適當的過渡語句，引導讀者理解證明的邏輯流程：

• "By assumption, ..."
• "It follows from Theorem X that ..."
• "Combining (1) and (2), we obtain ..."
• "Without loss of generality, ..."
• "By the definition of ..., we have ..."

常見警告

• 避免使用 "clearly"、"obviously"、"trivially" 來跳過步驟。
• 如果一個步驟需要超過三行的推導，考慮將其提取為獨立的引理。
• 確保所有變數在使用前已定義。
• 確保量詞 (for all, there exists) 的作用域明確。

品質檢查

• 每一步推導是否都有明確的邏輯依據？
• 是否有未說明的假設？
• 量詞的使用是否正確？
• 符號是否與論文其餘部分一致？
• 證明是否完整（以 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. 引用規範：使用的所有非本文證明的結果，都必須提供引用。