计划执行与检查节点
executing-plans
按既定实施计划完成工作,保持过程检查和反馈。
。\n- 展示公式使用 `\\[...\\]` 或有編號的環境。\n- 多行對齊使用 `align` 環境。\n- 分情況討論使用 `cases` 環境。\n\n### 輸出格式\n\n最終輸出應包含:\n\n1. 完整的 LaTeX 代碼片段(可直接複製貼上)\n2. 所需的額外套件列表(如 `amsthm`, `amsmath` 等)\n3. 如需自定義命令,附上 `\\newcommand` 定義\n\n### 品質檢查\n\n- [ ] LaTeX 代碼是否可以成功編譯?\n- [ ] 數學符號是否正確呈現?\n- [ ] 編號和引用是否正確?\n- [ ] 排版是否美觀(對齊、間距等)?\n- [ ] 是否符合目標期刊的格式要求?\n\n---\n\n## 符號與排版參考\n\n- [證明策略詳細說明](references/proof-strategies.md)\n- [定理連結方法](references/theorem-connection.md)\n- [符號慣例](references/notation-conventions.md)\n- [LaTeX 數學排版模式](references/latex-math-patterns.md)\n\n---\n\n## 使用範例\n\n### 範例一:簡單不等式證明\n\n**輸入**:證明對所有 $x > 0$,有 $e^x \\geq 1 + x$。\n\n**第一階段輸出**:\n\n```\n主張類型:Proposition\n前提條件:\n - x > 0, x ∈ ℝ\n結論:e^x ≥ 1 + x\n相關符號:e 為自然對數的底\n```\n\n**第三階段輸出**:\n\n```\n選擇策略:直接證明\n選擇理由:可通過分析 f(x) = e^x - 1 - x 的性質直接推導\n預期證明結構:\n 1. 定義 f(x) = e^x - 1 - x\n 2. 計算 f'(x) = e^x - 1\n 3. 分析 f 的單調性\n 4. 利用 f(0) = 0 得出結論\n預期難度:低\n```\n\n**第五階段輸出**:\n\n```latex\n\\begin{proposition}\n\\label{prop:exp-lower-bound}\n For all $x > 0$, we have $e^x \\geq 1 + x$.\n\\end{proposition}\n\n\\begin{proof}\n Define $f(x) = e^x - 1 - x$. We have $f(0) = 0$ and\n $f'(x) = e^x - 1 > 0$ for all $x > 0$. Therefore, $f$ is\n strictly increasing on $(0, \\infty)$, which implies\n $f(x) > f(0) = 0$ for all $x > 0$. That is, $e^x > 1 + x$.\n \\qed\n\\end{proof}\n```\n\n### 範例二:機器學習中的泛化界\n\n**輸入**:證明 PAC learning 框架下,有限假設類的樣本複雜度上界。\n\n**第一階段輸出**:\n\n```\n主張類型:Theorem\n前提條件:\n - H 為有限假設類,|H| \u003c ∞\n - 樣本 S 由分布 D 上的 m 個 i.i.d. 樣本組成\n - ε > 0, δ > 0\n結論:若 m ≥ (1/ε)(ln|H| + ln(1/δ)),則以機率至少 1-δ,\n 對所有 h ∈ H 有 |R(h) - R̂(h)| ≤ ε\n相關符號:R(h) 為真實風險,R̂(h) 為經驗風險\n```\n\n**第三階段輸出**:\n\n```\n選擇策略:直接證明 + 機率法\n輔助策略:歸約到 Hoeffding's inequality\n選擇理由:經典的 union bound + concentration inequality 組合\n預期證明結構:\n 1. 對單一假設 h 應用 Hoeffding's inequality\n 2. 對所有假設取 union bound\n 3. 解出 m 的下界\n預期難度:中\n```\n\n---\n\n## 常見工作模式\n\n### 模式一:完整證明撰寫\n\n用戶提供主張,系統執行完整的五階段流程,輸出可直接使用的 LaTeX 代碼。\n\n### 模式二:證明修復\n\n用戶提供有問題的證明,系統診斷問題所在並修復。常見問題包括:\n\n- 邏輯跳躍(缺少中間步驟)\n- 量詞錯誤\n- 邊界情況未處理\n- 引用的定理前提條件不滿足\n\n### 模式三:證明翻譯\n\n將非形式化的直覺論證轉換為嚴謹的數學證明。\n\n### 模式四:策略諮詢\n\n用戶描述要證明的目標,系統建議可能的證明策略和思路,但不撰寫完整證明。\n\n---\n\n## 注意事項\n\n1. **嚴謹性優先**:寧可冗長也不要跳步。讀者可以略過顯然的步驟,但無法填補\n 缺失的步驟。\n2. **符號一致性**:所有符號必須與論文其餘部分一致。如有衝突,在證明開頭明確\n 說明。參照 [符號慣例](references/notation-conventions.md)。\n3. **可編譯性**:輸出的 LaTeX 必須可以直接編譯,不能有語法錯誤。\n4. **學術語調**:使用正式的學術英文撰寫數學部分,避免口語化表達。\n5. **引用規範**:使用的所有非本文證明的結果,都必須提供引用。\n","licenseDocuments":[]}}
proof-writer【效率与协作】數學證明撰寫技能 — 從主張提取到 LaTeX 排版的完整證明工作流。當使用者需要撰寫或驗證數學定理、引理、命題的形式證明,或需要推導公式、整理理論分析時,一定要使用此技能。觸發詞包括:數學證明、prove、theorem、lemma、proposition、推導、理論分析、寫 proof、LaTeX 數學、formal proof。適用於機器學習理論、統計學習理論、最佳化等需要嚴謹數學推導的場景。
独立 GitHub 快照 · 自动分类 · 以原作者文档为准
本技能專注於學術論文中的數學證明撰寫。涵蓋從主張提取、策略選擇到完整 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 代碼。
用戶提供有問題的證明,系統診斷問題所在並修復。常見問題包括:
將非形式化的直覺論證轉換為嚴謹的數學證明。
用戶描述要證明的目標,系統建議可能的證明策略和思路,但不撰寫完整證明。