math-proof

# Math Proof 产出可审计的证明包；命题不成立或条件不足时，优先反驳或修正，不制造漂亮假证明。 ## Position in the Method Map 本 skill 位于“演绎验证 / 定理证明”的 proof-engineering 阶段，前置是 [`FORMAL-METHODS-MAP.md`](../../../governance/standards/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 ```text 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 证据。