--- name: proof-writer description: "數學證明撰寫技能 — 從主張提取到 LaTeX 排版的完整證明工作流。當使用者需要撰寫或驗證數學定理、引理、命題的形式證明，或需要推導公式、整理理論分析時，一定要使用此技能。觸發詞包括：數學證明、prove、theorem、lemma、proposition、推導、理論分析、寫 proof、LaTeX 數學、formal proof。適用於機器學習理論、統計學習理論、最佳化等需要嚴謹數學推導的場景。" license: MIT compatibility: Works with Claude Code, ChatGPT/Codex CLI, and Gemini CLI. metadata: author: weed version: "1.0.0" --- # proof-writer：數學證明撰寫技能 ## 概述 本技能專注於學術論文中的數學證明撰寫。涵蓋從主張提取、策略選擇到完整 LaTeX 排版的端對端工作流程。所有解釋使用繁體中文，數學表達式與 LaTeX 代碼使用英文。 --- ## 流程總覽 證明撰寫分為五個階段，依序執行： ``` 主張提取 → 文獻掃描 → 策略選擇 → 逐步推導 → LaTeX 排版 ``` 每個階段有明確的輸入、輸出與品質檢查點。以下逐一說明。 --- ## 第一階段：主張提取 ### 目的 從論文草稿或用戶輸入中，精確提取需要證明的數學主張。主張必須是形式化的命題， 具備明確的前提條件與結論。 ### 步驟 1. **辨識主張類型**：判斷是定理 (Theorem)、引理 (Lemma)、推論 (Corollary)、 命題 (Proposition)，還是聲明 (Claim)。 2. **提取前提條件**：列出所有假設、約束條件與適用範圍。 3. **提取結論**：明確寫出要證明的等式、不等式或性質。 4. **符號確認**：確認所有符號的定義與範圍，參照 [符號慣例](references/notation-conventions.md)。 5. **形式化陳述**：將主張寫成標準的數學陳述格式。 ### 輸出格式 ``` 主張類型：[Theorem | Lemma | Corollary | Proposition | Claim] 前提條件： - 條件 1 - 條件 2 - ... 結論：[形式化的數學陳述] 相關符號：[符號清單及定義] ``` ### 常見問題 - 前提條件不完整：回頭檢查論文中的假設段落。 - 符號未定義：查閱論文的 notation section 或向用戶確認。 - 主張過於模糊：要求用戶提供更精確的形式化陳述。 ### 品質檢查 - [ ] 主張是否為可判定的數學命題？ - [ ] 所有符號是否已定義？ - [ ] 前提條件是否足以推導結論？ - [ ] 主張類型是否正確分類？ --- ## 第二階段：文獻掃描 ### 目的 查找與主張相關的已知定理、引理和結果，為證明建立基礎。這一步決定了我們可以 「站在哪些巨人的肩膀上」。 ### 步驟 1. **關鍵詞提取**：從主張中提取數學關鍵詞（如 convergence、bound、 concentration inequality 等）。 2. **定理匹配**：在已知定理庫中搜索相關結果，參照 [定理連結方法](references/theorem-connection.md)。 3. **相關性評估**：評估每個找到的定理與當前主張的相關程度。 4. **依賴關係建立**：確定哪些定理可以直接使用，哪些需要適度修改。 5. **缺口分析**：找出已知結果與目標主張之間的差距。 ### 常用定理來源 - 論文自身前文已證明的引理 - 論文引用的參考文獻 - 領域內的經典結果（如 Cauchy-Schwarz, Jensen's inequality 等） - 標準教科書中的基礎定理 ### 輸出格式 ``` 相關定理： 1. [定理名稱] — [簡述] — 相關度：[高|中|低] 2. ... 可直接引用：[定理列表] 需要修改後使用：[定理列表及修改方向] 證明缺口：[需要自行推導的部分] ``` ### 品質檢查 - [ ] 是否遺漏了重要的已知結果？ - [ ] 引用的定理前提條件是否滿足？ - [ ] 定理的版本是否正確（有些定理有多個變體）？ --- ## 第三階段：策略選擇 ### 目的 根據主張的結構和可用的已知結果，選擇最合適的證明策略。策略的選擇直接影響 證明的清晰度和長度。 ### 可用策略 本技能支援以下八種證明策略，每種策略的詳細說明見 [證明策略參考](references/proof-strategies.md)。 #### 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 數學排版參考](references/latex-math-patterns.md)。 #### 基本環境 ```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 代碼是否可以成功編譯？ - [ ] 數學符號是否正確呈現？ - [ ] 編號和引用是否正確？ - [ ] 排版是否美觀（對齊、間距等）？ - [ ] 是否符合目標期刊的格式要求？ --- ## 符號與排版參考 - [證明策略詳細說明](references/proof-strategies.md) - [定理連結方法](references/theorem-connection.md) - [符號慣例](references/notation-conventions.md) - [LaTeX 數學排版模式](references/latex-math-patterns.md) --- ## 使用範例 ### 範例一：簡單不等式證明 **輸入**：證明對所有 $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 得出結論 預期難度：低 ``` **第五階段輸出**： ```latex \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. **符號一致性**：所有符號必須與論文其餘部分一致。如有衝突，在證明開頭明確 說明。參照 [符號慣例](references/notation-conventions.md)。 3. **可編譯性**：輸出的 LaTeX 必須可以直接編譯，不能有語法錯誤。 4. **學術語調**：使用正式的學術英文撰寫數學部分，避免口語化表達。 5. **引用規範**：使用的所有非本文證明的結果，都必須提供引用。