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 排版
每個階段有明確的輸入、輸出與品質檢查點。以下逐一說明。
第一階段:主張提取
目的
從論文草稿或用戶輸入中,精確提取需要證明的數學主張。主張必須是形式化的命題, 具備明確的前提條件與結論。
步驟
- 辨識主張類型:判斷是定理 (Theorem)、引理 (Lemma)、推論 (Corollary)、 命題 (Proposition),還是聲明 (Claim)。
- 提取前提條件:列出所有假設、約束條件與適用範圍。
- 提取結論:明確寫出要證明的等式、不等式或性質。
- 符號確認:確認所有符號的定義與範圍,參照 符號慣例。
- 形式化陳述:將主張寫成標準的數學陳述格式。
輸出格式
主張類型:[Theorem | Lemma | Corollary | Proposition | Claim]
前提條件:
- 條件 1
- 條件 2
- ...
結論:[形式化的數學陳述]
相關符號:[符號清單及定義]
常見問題
- 前提條件不完整:回頭檢查論文中的假設段落。
- 符號未定義:查閱論文的 notation section 或向用戶確認。
- 主張過於模糊:要求用戶提供更精確的形式化陳述。
品質檢查
- 主張是否為可判定的數學命題?
- 所有符號是否已定義?
- 前提條件是否足以推導結論?
- 主張類型是否正確分類?
第二階段:文獻掃描
目的
查找與主張相關的已知定理、引理和結果,為證明建立基礎。這一步決定了我們可以 「站在哪些巨人的肩膀上」。
步驟
- 關鍵詞提取:從主張中提取數學關鍵詞(如 convergence、bound、 concentration inequality 等)。
- 定理匹配:在已知定理庫中搜索相關結果,參照 定理連結方法。
- 相關性評估:評估每個找到的定理與當前主張的相關程度。
- 依賴關係建立:確定哪些定理可以直接使用,哪些需要適度修改。
- 缺口分析:找出已知結果與目標主張之間的差距。
常用定理來源
- 論文自身前文已證明的引理
- 論文引用的參考文獻
- 領域內的經典結果(如 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 散度等資訊論工具進行推導。
適用場景:通訊理論、學習理論下界、隱私分析。
策略選擇決策樹
主張結構分析
├─ 等式或不等式?
│ ├─ 是 → 考慮直接證明、凸性論證
│ └─ 否 → 繼續
├─ 存在性命題?
│ ├─ 是 → 考慮構造性證明、機率法
│ └─ 否 → 繼續
├─ 涉及遞迴或序列?
│ ├─ 是 → 考慮數學歸納法
│ └─ 否 → 繼續
├─ 可歸約為已知問題?
│ ├─ 是 → 考慮歸約法
│ └─ 否 → 繼續
├─ 涉及資訊量度?
│ ├─ 是 → 考慮資訊論方法
│ └─ 否 → 繼續
└─ 直接證明困難?
├─ 是 → 考慮反證法
└─ 否 → 使用直接證明
複合策略
許多複雜的證明需要組合多種策略。常見的組合包括:
- 歸納 + 直接:歸納步驟中使用直接證明
- 反證 + 構造:假設不存在,然後構造出矛盾的對象
- 歸約 + 資訊論:歸約到資訊論問題後使用資訊論工具
輸出格式
選擇策略:[主要策略名稱]
輔助策略:[如有]
選擇理由:[為什麼這個策略最適合]
預期證明結構:[大綱]
預期難度:[低|中|高]
第四階段:逐步推導
目的
根據選定的策略,撰寫完整、嚴謹的證明過程。每一步都必須有明確的邏輯依據。
原則
- 完整性:不跳過任何非顯而易見的步驟。
- 嚴謹性:每一步推導必須有明確的數學依據。
- 可讀性:使用清晰的語言引導讀者。
- 模組化:複雜的證明應拆分為多個引理。
撰寫規範
推導步驟格式
每一步推導應包含:
- 陳述:本步驟要建立的中間結論
- 推導:具體的數學推導過程
- 依據:引用的定理、引理或之前的步驟
過渡語句
在步驟之間使用適當的過渡語句,引導讀者理解證明的邏輯流程:
- "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環境。
輸出格式
最終輸出應包含:
- 完整的 LaTeX 代碼片段(可直接複製貼上)
- 所需的額外套件列表(如
amsthm,amsmath等) - 如需自定義命令,附上
\newcommand定義
品質檢查
- 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 代碼。
模式二:證明修復
用戶提供有問題的證明,系統診斷問題所在並修復。常見問題包括:
- 邏輯跳躍(缺少中間步驟)
- 量詞錯誤
- 邊界情況未處理
- 引用的定理前提條件不滿足
模式三:證明翻譯
將非形式化的直覺論證轉換為嚴謹的數學證明。
模式四:策略諮詢
用戶描述要證明的目標,系統建議可能的證明策略和思路,但不撰寫完整證明。
注意事項
- 嚴謹性優先:寧可冗長也不要跳步。讀者可以略過顯然的步驟,但無法填補 缺失的步驟。
- 符號一致性:所有符號必須與論文其餘部分一致。如有衝突,在證明開頭明確 說明。參照 符號慣例。
- 可編譯性:輸出的 LaTeX 必須可以直接編譯,不能有語法錯誤。
- 學術語調:使用正式的學術英文撰寫數學部分,避免口語化表達。
- 引用規範:使用的所有非本文證明的結果,都必須提供引用。