Back to Details

proof-writer

Compare original and translation side by side

🇺🇸

Original

English
🇨🇳

Translation

Chinese

Proof Write: Rigorous Theorem / Lemma Drafting

证明撰写：严谨的Theorem/Lemma起草

Write a mathematically honest proof package, not a polished fake proof.
撰写数学上真实可信的证明包，而非虚假的精美证明。

Constants

常量

  • DEFAULT_PROOF_DOC = 
    PROOF_PACKAGE.md
    in project root
  • STATUS = 
    PROVABLE AS STATED | PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION | NOT CURRENTLY JUSTIFIED
  • DEFAULT_PROOF_DOC = 项目根目录下的
    PROOF_PACKAGE.md
  • STATUS = 
    PROVABLE AS STATED | PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION | NOT CURRENTLY JUSTIFIED

Context: $ARGUMENTS

上下文：$ARGUMENTS

Goal

目标

Produce exactly one of:
  1. a complete proof of the original claim
  2. a corrected claim plus a proof of the corrected claim
  3. a blockage report explaining why the claim is not currently justified
生成以下内容之一：
  1. 原声明的完整证明
  2. 修正后的声明及其证明
  3. 阻塞报告，解释为何该声明目前无法被证明

Inputs

输入

Extract and normalize:
  • exact theorem / lemma / proposition / corollary statement
  • explicit assumptions
  • notation and definitions
  • any user-provided proof sketch, partial proof, or intended strategy
  • nearby lemmas or claims in local notes, appendix files, or theorem drafts if the request points to them
  • desired output style if specified: concise, appendix-ready, or full-detail
If notation or assumptions are ambiguous, state the exact interpretation you are using before proving anything.
提取并规范化：
  • 确切的Theorem/Lemma/Proposition/Corollary陈述
  • 明确的假设
  • 符号和定义
  • 用户提供的任何证明草图、部分证明或预期策略
  • 如果请求指向本地笔记、附录文件或定理草稿中的相关引理或声明，也需提取
  • 若指定了所需输出风格：简洁版、适合附录版或详细完整版
如果符号或假设存在歧义，请在开始证明前说明你使用的确切解释。

Workflow

工作流程

Step 1: Gather Proof Context

步骤1：收集证明上下文

Determine the target proof file with this priority:
  1. a file path explicitly specified by the user
  2. a proof draft already referenced in local notes or theorem files
  3. PROOF_PACKAGE.md
    in project root as the default target
Read the relevant local context:
  • the chosen target proof file, if it already exists
  • theorem notes, appendix drafts, or files explicitly mentioned by the user
Extract:
  • exact claim
  • assumptions
  • notation
  • proof sketch or partial proof
  • nearby lemmas that the draft may depend on
按以下优先级确定目标证明文件：
  1. 用户明确指定的文件路径
  2. 本地笔记或定理文件中已引用的证明草稿
  3. 默认使用项目根目录下的
    PROOF_PACKAGE.md
读取相关本地上下文：
  • 所选的目标证明文件（若已存在）
  • 用户明确提及的定理笔记、附录草稿或文件
提取：
  • 确切声明
  • 假设
  • 符号
  • 证明草图或部分证明
  • 草稿可能依赖的相关引理

Step 2: Normalize the Claim

步骤2：规范化声明

Restate:
  • the exact claim being proved
  • all assumptions, separately from conclusions
  • all symbols used in the claim
Identify:
  • hidden assumptions
  • undefined notation
  • scope ambiguities
  • whether the available sketch proves the full claim or only a weaker variant
Preserve the user's original theorem statement unless a change is explicitly required. If you use a stronger normalization or cleaner internal formulation only to make the proof easier, keep that as an internal proof device rather than silently replacing the original claim.
重述：
  • 待证明的确切声明
  • 所有假设（与结论分开列出）
  • 声明中使用的所有符号
识别：
  • 隐藏假设
  • 未定义的符号
  • 范围歧义
  • 现有草图是否能证明完整声明，还是仅能证明较弱的变体
除非明确需要修改，否则保留用户的原始定理陈述。 若为简化证明而使用了更强的规范化或更清晰的内部表述，请将其仅作为内部证明工具，而非悄悄替换原始声明。

Step 3: Feasibility Triage

步骤3：可行性分类

Before writing a proof, classify the claim into exactly one status:
  • PROVABLE AS STATED
  • PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION
  • NOT CURRENTLY JUSTIFIED
Check explicitly:
  • does the conclusion actually follow from the listed assumptions?
  • is any cited theorem being used outside its conditions?
  • is the claim stronger than what the available argument supports?
  • is there an obvious counterexample, boundary case, or quantifier failure?
If the claim is not provable as stated, do NOT fabricate a proof. Do NOT silently strengthen assumptions or narrow the theorem's scope just to make the proof work.
在撰写证明前，将声明精确分类为以下状态之一：
  • PROVABLE AS STATED
  • PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION
  • NOT CURRENTLY JUSTIFIED
明确检查：
  • 结论是否真的能从列出的假设推导得出？
  • 是否在条件之外引用了任何定理？
  • 声明是否比现有论证所能支持的更强？
  • 是否存在明显的反例、边界情况或量词错误？
如果声明无法按原陈述证明，请勿编造证明。 请勿为了完成证明而悄悄强化假设或缩小定理的适用范围。

Step 4: Build a Dependency Map

步骤4：构建依赖图

Choose a proof strategy, for example:
  • direct
  • contradiction
  • induction
  • construction
  • reduction to a known result
  • coupling / probabilistic argument
  • optimization inequality chaining
Then write a dependency map:
  • main claim
  • required intermediate lemmas
  • named theorems or inequalities that will be cited
  • which assumptions each nontrivial step depends on
  • boundary cases that must be handled separately
If one step is substantial, isolate it as a lemma instead of burying it in one sentence.
选择一种证明策略，例如：
  • 直接证明
  • 反证法
  • 归纳法
  • 构造法
  • 归约为已知结论
  • 耦合/概率论证
  • 优化不等式链
然后撰写依赖图：
  • 主声明
  • 所需的中间引理
  • 将引用的命名定理或不等式
  • 每个非平凡步骤依赖的假设
  • 必须单独处理的边界情况
如果某一步骤内容较多，请将其作为引理单独列出，而非隐藏在一句话中。

Step 5: Write the Proof Document

步骤5：撰写证明文档

Write to the chosen target proof file.
If the target proof file already exists:
  • read it first
  • update the relevant claim section
  • do not blindly duplicate prior content
If the user does not specify a target, default to 
PROOF_PACKAGE.md
in project root.
Do NOT write directly into paper sections or appendix 
.tex
files unless the user explicitly asks for that target.
The proof package must include:
  • exact claim
  • explicit assumptions
  • proof status
  • announced strategy
  • dependency map
  • numbered major steps
  • justification for every nontrivial implication
Mathematical rigor requirements:
  • never use "clearly", "obviously", "it can be shown", "by standard arguments", or "similarly" to hide a gap
  • define every constant and symbol before use
  • check quantifier order carefully
  • handle degenerate and boundary cases explicitly, or state why they are excluded
  • if invoking a standard fact, state its name and why its assumptions are satisfied here
  • use 
    $...$
    for inline math and 
    $$...$$
    for display equations
  • never write math in plain text
  • if the proof uses an equivalent normalization that is stronger in appearance than the user's original theorem statement, label it explicitly as a proof device and keep the original claim separate
写入所选的目标证明文件。
若目标证明文件已存在：
  • 先读取该文件
  • 更新相关声明部分
  • 不要盲目重复已有内容
若用户未指定目标文件，默认使用项目根目录下的
PROOF_PACKAGE.md
。 除非用户明确要求，否则请勿直接写入论文章节或附录的
.tex
文件。
证明包必须包含：
  • 确切声明
  • 明确的假设
  • 证明状态
  • 声明的策略
  • 依赖图
  • 编号的主要步骤
  • 每个非平凡推导的依据
数学严谨性要求：
  • 绝不使用“显然”“易见”“可证得”“通过标准论证”或“类似地”来掩盖漏洞
  • 在使用前定义每个常量和符号
  • 仔细检查量词顺序
  • 明确处理退化情况和边界情况，或说明为何将其排除
  • 若引用标准结论，需说明其名称及为何此处满足其假设条件
  • 行内数学公式使用
    $...$
    ，显示公式使用
    $$...$$
  • 绝不使用纯文本编写数学内容
  • 若证明使用了比用户原始定理陈述看起来更强的等效规范化形式，请明确将其标记为证明工具，并与原始声明分开

Step 6: Final Verification

步骤6：最终验证

Before finishing the target proof file, verify:
  • the theorem statement exactly matches what was actually shown
  • every assumption used is stated
  • every nontrivial implication is justified
  • every inequality direction is correct
  • every cited result is applicable under the stated assumptions
  • edge cases are handled or explicitly excluded
  • no hidden dependence on an unproved lemma remains
If a key step still cannot be justified, downgrade the status and write a blockage report instead of forcing a proof.
在完成目标证明文件前，验证：
  • 定理陈述与实际证明的内容完全一致
  • 使用的所有假设均已列出
  • 每个非平凡推导均有依据
  • 每个不等式的方向均正确
  • 引用的每个结论在给定假设下均适用
  • 边界情况已处理或明确排除
  • 不存在对未证明引理的隐藏依赖
若关键步骤仍无法证明，请降级状态并撰写阻塞报告，而非强行完成证明。

Required File Structure

要求的文件结构

Write the target proof file using this structure:
md
undefined
使用以下结构撰写目标证明文件：
md
undefined

Proof Package

Proof Package

Claim

Claim

[exact statement]
[确切陈述]

Status

Status

PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED
PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED

Assumptions

Assumptions

  • ...
  • ...

Notation

Notation

  • ...
  • ...

Proof Strategy

Proof Strategy

[chosen approach and why]
[所选方法及原因]

Dependency Map

Dependency Map

  1. Main claim depends on ...
  2. Lemma A depends on ...
  3. Step k uses ...
  1. 主声明依赖于...
  2. 引理A依赖于...
  3. 步骤k使用...

Proof

Proof

Step 1. ... Step 2. ... ... Therefore the claim follows. ∎
Step 1. ... Step 2. ... ... Therefore the claim follows. ∎

Corrections or Missing Assumptions

Corrections or Missing Assumptions

  • [only if needed]
  • [仅在需要时填写]

Open Risks

Open Risks

  • [remaining fragile points, if any]
undefined
  • [若有，列出剩余的不确定点]
undefined

Output Modes

输出模式

If the claim is provable as stated

若声明可按原陈述证明

Write the full file structure above with a complete proof.
撰写上述完整文件结构及完整证明。

If the original claim is too strong

若原始声明过强

Write:
  • why the original statement is not justified
  • the corrected claim
  • the minimal extra assumption if one exists
  • a proof of the corrected claim
撰写：
  • 为何原始陈述无法成立
  • 修正后的声明
  • 若存在，最小的额外假设
  • 修正后声明的证明

If the proof cannot be completed honestly

若无法真实完成证明

Write:
  • Status: NOT CURRENTLY JUSTIFIED
  • the exact blocker: missing lemma, invalid implication, hidden assumption, or counterexample direction
  • what extra assumption, lemma, or derivation would be needed to finish the proof
  • a corrected weaker statement if one is available
撰写：
  • Status: NOT CURRENTLY JUSTIFIED
  • 确切的阻塞点：缺失的引理、无效的推导、隐藏的假设或反例方向
  • 完成证明所需的额外假设、引理或推导
  • 若存在，修正后的较弱陈述

Chat Response

聊天响应

After writing the target proof file, respond briefly with:
  • status
  • whether the original claim survived unchanged
  • what file was updated
完成目标证明文件后，简要回复：
  • 状态
  • 原始声明是否保持不变
  • 更新了哪个文件

Key Rules

核心规则

  • Never fabricate a missing proof step.
  • Prefer weakening the claim over overclaiming.
  • Separate assumptions, derived facts, heuristics, and conjectures.
  • Preserve the user's original theorem statement unless you explicitly mark a corrected claim or an internal normalization.
  • If the statement is false as written, say so explicitly and give a counterexample or repaired statement.
  • If uncertainty remains, mark it explicitly in 
    Open Risks
    ; do not hide it inside polished prose.
  • Correctness matters more than brevity.
  • 绝不编造缺失的证明步骤。
  • 优先弱化声明而非过度声称。
  • 区分假设、推导结论、启发式方法和猜想。
  • 除非明确标记修正后的声明或内部规范化形式，否则保留用户的原始定理陈述。
  • 若原陈述为假，请明确说明并给出反例或修正后的陈述。
  • 若仍存在不确定性，请在
    Open Risks
    中明确标记；不要隐藏在精美的文字中。
  • 正确性比简洁性更重要。