tradecatlabs Math Proof
产出可审计的证明包；命题不成立或条件不足时，优先反驳或修正，不制造漂亮假证明。
Position in the Method Map
本 skill 位于“演绎验证 / 定理证明”的 proof-engineering 阶段，前置是 FORMAL-METHODS-MAP.md 所定义的规格与语义边界。证明草稿、引理图和自然语言审查不会自动等同于 Lean kernel check；需要形式化时交给 math-formalization，需要有限反例或 SMT 路径时交给 math-computation。
When to Use This Skill
- 用户要求证明、补全或检查一个数学命题。
- 当前证明含“显然”“类似”“标准论证”等可能隐藏缺口的跳步。
- 需要将大结论拆成引理、证明义务和依赖图。
- 需要从边界值、退化情形或量词顺序寻找反例。
Not For / Boundaries
- 候选库条目必须先形成精确用户请求或 active ProblemContract；来源状态、目录题面或 candidate formal file 不能触发研究证明或 Result 晋升。
- 自然语言证明只能达到
proof-drafted或经真实人工审查后的human-reviewed。 kernel-checked只由math-formalization的真实 proof assistant 成功证据产生。- 不静默强化假设、缩小定义域或改变结论量词。
- 引用标准定理时必须说明名称、版本/来源和为何满足前提。
- 证明义务图出现重复 ID、未知依赖、循环或未闭合节点时必须 fail-closed，不能 warning 后继续。
- 子引理被反驳只否定当前证明路线；除非反例直接满足原命题的否定，不能把原命题标记
refuted。
Quick Reference
Claim：精确陈述与量词顺序。
Status：provable-as-stated / repaired / refuted / blocked。
Assumptions：显式、隐藏和最小必要条件。
Proof obligations：每个非平凡蕴含一个义务。
Dependency map：结论 -> 引理 -> 外部定理 -> 假设。
Graph gate：节点 ID 唯一、依赖存在、无环、所有终点可追溯到 Claim。
Attack pass：边界、退化、极端尺度、量词交换、等号条件。
Proof：编号步骤，每步绑定义务或已验证结果。
Open gaps：任何未闭合项都会阻止完成声明。
Route status：open / blocked / refuted / closed，与 Claim status 分开记录。
Examples
Example 1：命题为假
- 输入：一个全称不等式。
- 动作：先检查边界和小规模反例，再决定证明策略。
- 验收：找到反例后停止写证明，输出最小反例和可能修正版。
Example 2：缺少紧致性
- 输入：证明草稿在极值存在性处跳步。
- 动作：隔离存在性义务，核查连续性、闭性和有界性。
- 验收：条件不足时状态为 repaired/blocked，不写“显然存在”。
Example 3：完整证明草稿
- 输入：陈述、假设与若干已知引理。
- 动作：建立依赖图，逐项闭合证明义务并做反例攻击。
- 验收：statement 与实际证明完全一致，仍标记
proof-drafted而非 kernel-checked。
Example 4：路线引理为假
- 输入：某条证明路线依赖一个可被反例推翻的辅助引理。
- 动作：将该 route 标记 refuted，检查反例是否也反驳原 Claim，并保留其他独立路线。
- 验收：没有原命题反例时，Claim 仍为 blocked/open，而不是 refuted。
References
references/source-map.md：证明、审稿、proof DAG 与批判性思考来源映射。references/pressure-tests.md：错误命题、DAG 完整性、路线状态与隐藏缺口压力场景。
Maintenance
- Sources：
annals-of-mathematics-skills、kdense-scientific-skills、proofflow、leanprover-skills；上游图与 skill 只作方法/反例来源，不代表本项目已安装或验证。 - Last updated：2026-08-26。
- Verification：项目结构校验；数学正确性需要人工或 proof assistant 证据。