數學證明撰寫技能 — 從主張提取到 LaTeX 排版的完整證明工作流。當使用者需要撰寫或驗證數學定理、引理、命題的形式證明,或需要推導公式、整理理論分析時,一定要使用此技能。觸發詞包括:數學證明、prove、theorem、lemma、proposition、推導、理論分析、寫 proof、LaTeX 數學、formal proof。適用於機器學習理論、統計學習理論、最佳化等需要嚴謹數學推導的場景。
本技能專注於學術論文中的數學證明撰寫。涵蓋從主張提取、策略選擇到完整 LaTeX 排版的端對端工作流程。所有解釋使用繁體中文,數學表達式與 LaTeX 代碼使用英文。
證明撰寫分為五個階段,依序執行:
主張提取 → 文獻掃描 → 策略選擇 → 逐步推導 → LaTeX 排版
每個階段有明確的輸入、輸出與品質檢查點。以下逐一說明。
從論文草稿或用戶輸入中,精確提取需要證明的數學主張。主張必須是形式化的命題, 具備明確的前提條件與結論。
主張類型:[Theorem | Lemma | Corollary | Proposition | Claim]
前提條件:
- 條件 1
- 條件 2
- ...
結論:[形式化的數學陳述]
相關符號:[符號清單及定義]
查找與主張相關的已知定理、引理和結果,為證明建立基礎。這一步決定了我們可以 「站在哪些巨人的肩膀上」。
相關定理:
1. [定理名稱] — [簡述] — 相關度:[高|中|低]
2. ...
可直接引用:[定理列表]
需要修改後使用:[定理列表及修改方向]
證明缺口:[需要自行推導的部分]
根據主張的結構和可用的已知結果,選擇最合適的證明策略。策略的選擇直接影響 證明的清晰度和長度。
本技能支援以下八種證明策略,每種策略的詳細說明見 證明策略參考。
從前提條件出發,通過一系列邏輯推導直接到達結論。適用於結構清晰、推導路徑 明確的主張。
適用場景:等式證明、不等式推導、集合包含關係。
假設結論不成立,推導出矛盾。適用於直接證明困難或結論為否定形式的主張。
適用場景:存在性的否定、唯一性證明、不可能性結果。
對自然數或可良序化的結構進行歸納。包括弱歸納、強歸納和結構歸納。
適用場景:遞迴結構、序列性質、離散數學中的命題。
明確構造出滿足條件的對象,從而證明存在性。比純存在性證明提供更多資訊。
適用場景:存在性命題、算法正確性、具體界的建立。
將要證明的問題歸約為已知的問題。常用於計算複雜度和決策問題。
適用場景:NP-hardness 證明、下界證明、等價性證明。
通過證明隨機選擇滿足條件的機率大於零,從而證明滿足條件的對象存在。
適用場景:組合數學、圖論、隨機化算法分析。
利用凸函數或凸集的性質進行推導。在最佳化和機器學習理論中尤其常見。
適用場景:最佳化問題、Jensen's inequality 的應用、凸鬆弛。
使用熵、互資訊、KL 散度等資訊論工具進行推導。
適用場景:通訊理論、學習理論下界、隱私分析。
主張結構分析
├─ 等式或不等式?
│ ├─ 是 → 考慮直接證明、凸性論證
│ └─ 否 → 繼續
├─ 存在性命題?
│ ├─ 是 → 考慮構造性證明、機率法
│ └─ 否 → 繼續
├─ 涉及遞迴或序列?
│ ├─ 是 → 考慮數學歸納法
│ └─ 否 → 繼續
├─ 可歸約為已知問題?
│ ├─ 是 → 考慮歸約法
│ └─ 否 → 繼續
├─ 涉及資訊量度?
│ ├─ 是 → 考慮資訊論方法
│ └─ 否 → 繼續
└─ 直接證明困難?
├─ 是 → 考慮反證法
└─ 否 → 使用直接證明
許多複雜的證明需要組合多種策略。常見的組合包括:
選擇策略:[主要策略名稱]
輔助策略:[如有]
選擇理由:[為什麼這個策略最適合]
預期證明結構:[大綱]
預期難度:[低|中|高]
根據選定的策略,撰寫完整、嚴謹的證明過程。每一步都必須有明確的邏輯依據。
每一步推導應包含:
在步驟之間使用適當的過渡語句,引導讀者理解證明的邏輯流程:
將證明轉換為可直接插入論文的 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 環境。最終輸出應包含:
amsthm, amsmath 等)\newcommand 定義輸入:證明對所有 $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 代碼。
用戶提供有問題的證明,系統診斷問題所在並修復。常見問題包括:
將非形式化的直覺論證轉換為嚴謹的數學證明。
用戶描述要證明的目標,系統建議可能的證明策略和思路,但不撰寫完整證明。