proof-writer

Proof Write：严谨的定理／引理起草

撰写一份数学上诚实的证明材料，而不是一份看似完善却虚假的证明。

常量

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

上下文：$ARGUMENTS

目标

准确产出以下内容之一：

1. 对原命题的完整证明
2. 修正后的命题及其证明
3. 说明该命题目前为何尚无充分依据的阻碍报告

输入

提取并规范化以下内容：

• 定理／引理／命题／推论的准确表述
• 明确的假设
• 符号和定义
• 用户提供的证明概要、部分证明或预期策略
• 如果请求中提及相关内容，则包括本地笔记、附录文件或定理草稿中的相关引理或命题
• 如果指定了所需的输出风格，则包括简洁版、可用于附录的版本或详细版

如果符号或假设存在歧义，请在开始证明前说明所采用的确切解释。

工作流程

步骤 1：收集证明上下文

按以下优先级确定目标证明文件：

1. 用户明确指定的文件路径
2. 本地笔记或定理文件中已引用的证明草稿
3. 项目根目录中的 PROOF_PACKAGE.md，作为默认目标文件

阅读相关的本地上下文：

• 已存在时，阅读选定的目标证明文件
• 阅读定理笔记、附录草稿或用户明确提及的文件

提取：

• 准确的命题
• 假设
• 符号
• 证明概要或部分证明
• 草稿可能依赖的相关引理

步骤 2：规范化命题

重述以下内容：

• 正在证明的准确命题
• 与结论分开列出的所有假设
• 命题中使用的所有符号

识别：

• 隐含假设
• 未定义的符号
• 范围歧义
• 现有概要证明的是完整命题，还是仅证明了较弱的变体

除非明确需要更改，否则保留用户的原始定理表述。 如果为了简化证明而使用更强的规范化表述或更简洁的内部表述，请仅将其作为内部证明手段，不得在未说明的情况下替换原命题。

可选的 Lean 证明路线

当用户要求使用 Lean，或将特定证明义务形式化有助于实质性地确立正确性时，请携带原始表述、当前尝试和已知依赖项调用 /lean-formalize。它既会推导证明，也会完成其形式化实现。将已验证的范围、导出的定理和剩余义务返回给此证明材料。部分结果只能完成与其对应的义务。如果 lean-formalize 为补充缺失的数学论证而调用此流程，请将该论证及剩余缺口返回给发起调用的 Lean 运行；不要递归调用 lean-formalize。常规证明起草无需使用 Lean；仅有难度本身并不足以触发调用。

步骤 3：可行性分类

在撰写证明之前，必须将命题准确归入以下一种状态：

• PROVABLE AS STATED
• PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION
• NOT CURRENTLY JUSTIFIED

明确检查：

• 结论是否确实能从所列假设推出？
• 是否在引用定理时违反了其适用条件？
• 命题是否强于现有论证所能支持的范围？
• 是否存在明显的反例、边界情形或量词问题？

如果命题无法按原样证明，切勿编造证明。 切勿为了让证明成立而暗中加强假设或缩小定理的适用范围。

步骤 4：构建依赖关系图

选择一种证明策略，例如：

• 直接证明
• 反证法
• 归纳法
• 构造法
• 化归为已知结果
• 耦合／概率论证
• 优化不等式链式推导

然后编写依赖关系图：

• 主要结论
• 所需的中间引理
• 将引用的定理或不等式名称
• 每个非平凡步骤所依赖的假设
• 必须单独处理的边界情况

如果某个步骤内容较多，应将其单独列为引理，而不是把它塞进一句话里。

步骤 5：编写证明文档

写入选定的目标证明文件。

如果目标证明文件已存在：

• 先阅读该文件
• 更新相关的结论部分
• 不要盲目重复已有内容

如果用户未指定目标文件，默认使用项目根目录下的 PROOF_PACKAGE.md。

除非用户明确指定该目标，否则不要直接写入论文正文部分或附录 .tex 文件。

证明包必须包括：

• 精确的结论
• 明确的假设
• 证明状态
• 声明采用的策略
• 依赖关系图
• 编号的主要步骤
• 对每个非平凡推论的论证

数学严谨性要求：

• 绝不要用“显然”“不言而喻”“可以证明”“根据标准论证”或“类似地”来掩盖推理缺口
• 使用前先定义每个常数和符号
• 仔细检查量词顺序
• 明确处理退化情况和边界情况，或说明排除它们的理由
• 如果引用标准事实，说明其名称以及为何此处满足其适用条件
• 行内数学使用 $...$，陈列数学使用 $$...$$
• 绝不要用纯文本书写数学公式
• 如果证明使用的等价归一化在表面上比用户原始定理陈述更强，应明确将其标注为证明手段，并将原始结论单独保留

步骤 6：最终核验

完成目标证明文件前，核验以下内容：

• 定理陈述与实际证明的内容完全一致
• 所用的每项假设都已写明
• 每个非平凡推论都有论证
• 每个不等式的方向都正确
• 每个引用的结果在所述假设下都适用
• 已处理边界情况，或明确说明将其排除
• 不存在依赖未证明引理的隐含步骤

如果关键步骤仍无法论证，应降低状态并撰写阻碍报告，而不是强行给出证明。

必需的文件结构

使用以下结构编写目标证明文件：

# Proof Package

## Claim
[exact statement]

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

## Assumptions
- ...

## Notation
- ...

## Proof Strategy
[chosen approach and why]

## Dependency Map
1. Main claim depends on ...
2. Lemma A depends on ...
3. Step k uses ...

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

## Corrections or Missing Assumptions
- [only if needed]

## Open Risks
- [remaining fragile points, if any]

输出模式

如果结论按原样可证

使用上述完整文件结构，并给出完整证明。

如果原始结论过强

写明：

• 原陈述为何缺乏依据
• 修正后的结论
• 若存在，所需的最小额外假设
• 修正后结论的证明

如果无法诚实地完成证明

写明：

• Status: NOT CURRENTLY JUSTIFIED
• 确切的阻碍：缺失的引理、无效推论、隐含假设或反例方向
• 完成证明所需的额外假设、引理或推导
• 如果存在，修正后的较弱陈述

聊天回复

写好目标证明文件后，简要回复：

• 状态
• 原始结论是否原样成立
• 更新了哪个文件

关键规则

• 绝不捏造缺失的证明步骤。
• 与其夸大结论，不如优先弱化结论。
• 区分假设、推导出的事实、启发式判断和猜想。
• 保留用户的原始定理陈述，除非你明确标注了修正后的结论或内部归一化。
• 如果陈述按原样不成立，应明确说明，并给出反例或修正后的陈述。
• 如果仍有不确定性，应在 Open Risks 中明确标注；不要把它藏在看似完善的表述中。
• 正确性比简洁更重要。